MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcoteq1a Structured version   Visualization version   GIF version

Theorem sbcoteq1a 8049
Description: Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024.)
Assertion
Ref Expression
sbcoteq1a (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1st ‘(1st𝐴)) / 𝑥][(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑𝜑))

Proof of Theorem sbcoteq1a
StepHypRef Expression
1 fveq2 6891 . . . 4 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (2nd𝐴) = (2nd ‘⟨𝑥, 𝑦, 𝑧⟩))
2 ot3rdg 8003 . . . . 5 (𝑧 ∈ V → (2nd ‘⟨𝑥, 𝑦, 𝑧⟩) = 𝑧)
32elv 3475 . . . 4 (2nd ‘⟨𝑥, 𝑦, 𝑧⟩) = 𝑧
41, 3eqtr2di 2784 . . 3 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → 𝑧 = (2nd𝐴))
5 sbceq1a 3785 . . 3 (𝑧 = (2nd𝐴) → (𝜑[(2nd𝐴) / 𝑧]𝜑))
64, 5syl 17 . 2 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (𝜑[(2nd𝐴) / 𝑧]𝜑))
7 2fveq3 6896 . . . 4 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (2nd ‘(1st𝐴)) = (2nd ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)))
8 vex 3473 . . . . 5 𝑥 ∈ V
9 vex 3473 . . . . 5 𝑦 ∈ V
10 vex 3473 . . . . 5 𝑧 ∈ V
11 ot2ndg 8002 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (2nd ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)) = 𝑦)
128, 9, 10, 11mp3an 1458 . . . 4 (2nd ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)) = 𝑦
137, 12eqtr2di 2784 . . 3 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → 𝑦 = (2nd ‘(1st𝐴)))
14 sbceq1a 3785 . . 3 (𝑦 = (2nd ‘(1st𝐴)) → ([(2nd𝐴) / 𝑧]𝜑[(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑))
1513, 14syl 17 . 2 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(2nd𝐴) / 𝑧]𝜑[(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑))
16 2fveq3 6896 . . . 4 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (1st ‘(1st𝐴)) = (1st ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)))
17 ot1stg 8001 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (1st ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)) = 𝑥)
188, 9, 10, 17mp3an 1458 . . . 4 (1st ‘(1st ‘⟨𝑥, 𝑦, 𝑧⟩)) = 𝑥
1916, 18eqtr2di 2784 . . 3 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → 𝑥 = (1st ‘(1st𝐴)))
20 sbceq1a 3785 . . 3 (𝑥 = (1st ‘(1st𝐴)) → ([(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑[(1st ‘(1st𝐴)) / 𝑥][(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑))
2119, 20syl 17 . 2 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑[(1st ‘(1st𝐴)) / 𝑥][(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑))
226, 15, 213bitrrd 306 1 (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1st ‘(1st𝐴)) / 𝑥][(2nd ‘(1st𝐴)) / 𝑦][(2nd𝐴) / 𝑧]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wcel 2099  Vcvv 3469  [wsbc 3774  cotp 4632  cfv 6542  1st c1st 7985  2nd c2nd 7986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-ot 4633  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fv 6550  df-1st 7987  df-2nd 7988
This theorem is referenced by:  ralxp3es  8138  frpoins3xp3g  8140
  Copyright terms: Public domain W3C validator