Theorem sbcoteq1a 33220

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

Step	Hyp	Ref	Expression
1		opex 5329	. . . . 5 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		vex 3414	. . . . 5 ⊢ 𝑧 ∈ V
3	1, 2	op2ndd 7711	. . . 4 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (2nd ‘𝐴) = 𝑧)
4	3	eqcomd 2765	. . 3 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑧 = (2nd ‘𝐴))
5		sbceq1a 3710	. . 3 ⊢ (𝑧 = (2nd ‘𝐴) → (𝜑 ↔ [(2nd ‘𝐴) / 𝑧]𝜑))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 ↔ [(2nd ‘𝐴) / 𝑧]𝜑))
7		vex 3414	. . . . 5 ⊢ 𝑥 ∈ V
8		vex 3414	. . . . 5 ⊢ 𝑦 ∈ V
9	7, 8, 2	ot22ndd 33214	. . . 4 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (2nd ‘(1st ‘𝐴)) = 𝑦)
10	9	eqcomd 2765	. . 3 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑦 = (2nd ‘(1st ‘𝐴)))
11		sbceq1a 3710	. . 3 ⊢ (𝑦 = (2nd ‘(1st ‘𝐴)) → ([(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑))
12	10, 11	syl 17	. 2 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑))
13	7, 8, 2	ot21std 33213	. . . 4 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (1st ‘(1st ‘𝐴)) = 𝑥)
14	13	eqcomd 2765	. . 3 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑥 = (1st ‘(1st ‘𝐴)))
15		sbceq1a 3710	. . 3 ⊢ (𝑥 = (1st ‘(1st ‘𝐴)) → ([(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑))
16	14, 15	syl 17	. 2 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ [(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑))
17	6, 12, 16	3bitrrd 309	1 ⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539  [wsbc 3699  ⟨cop 4532  ‘cfv 6341  1^st c1st 7698  2^nd c2nd 7699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pr 5303  ax-un 7466

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3700  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-iota 6300  df-fun 6343  df-fv 6349  df-1st 7700  df-2nd 7701

This theorem is referenced by:  ralxp3es  33221  frpoins3xp3g  33347