Theorem sbccomlem 3116

Description: Lemma for sbccom 3117. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)

Assertion

Ref	Expression
sbccomlem	⊢ ([̣A / x]̣[̣B / y]̣φ ↔ [̣B / y]̣[̣A / x]̣φ)

Distinct variable groups:   x,y,A   x,B,y

Allowed substitution hints:   φ(x,y)

Proof of Theorem sbccomlem

Step	Hyp	Ref	Expression
1		excom 1741	. . . 4 ⊢ (∃x∃y(x = A ∧ (y = B ∧ φ)) ↔ ∃y∃x(x = A ∧ (y = B ∧ φ)))
2		exdistr 1906	. . . 4 ⊢ (∃x∃y(x = A ∧ (y = B ∧ φ)) ↔ ∃x(x = A ∧ ∃y(y = B ∧ φ)))
3		an12 772	. . . . . . 7 ⊢ ((x = A ∧ (y = B ∧ φ)) ↔ (y = B ∧ (x = A ∧ φ)))
4	3	exbii 1582	. . . . . 6 ⊢ (∃x(x = A ∧ (y = B ∧ φ)) ↔ ∃x(y = B ∧ (x = A ∧ φ)))
5		19.42v 1905	. . . . . 6 ⊢ (∃x(y = B ∧ (x = A ∧ φ)) ↔ (y = B ∧ ∃x(x = A ∧ φ)))
6	4, 5	bitri 240	. . . . 5 ⊢ (∃x(x = A ∧ (y = B ∧ φ)) ↔ (y = B ∧ ∃x(x = A ∧ φ)))
7	6	exbii 1582	. . . 4 ⊢ (∃y∃x(x = A ∧ (y = B ∧ φ)) ↔ ∃y(y = B ∧ ∃x(x = A ∧ φ)))
8	1, 2, 7	3bitr3i 266	. . 3 ⊢ (∃x(x = A ∧ ∃y(y = B ∧ φ)) ↔ ∃y(y = B ∧ ∃x(x = A ∧ φ)))
9		sbc5 3070	. . 3 ⊢ ([̣A / x]̣∃y(y = B ∧ φ) ↔ ∃x(x = A ∧ ∃y(y = B ∧ φ)))
10		sbc5 3070	. . 3 ⊢ ([̣B / y]̣∃x(x = A ∧ φ) ↔ ∃y(y = B ∧ ∃x(x = A ∧ φ)))
11	8, 9, 10	3bitr4i 268	. 2 ⊢ ([̣A / x]̣∃y(y = B ∧ φ) ↔ [̣B / y]̣∃x(x = A ∧ φ))
12		sbc5 3070	. . 3 ⊢ ([̣B / y]̣φ ↔ ∃y(y = B ∧ φ))
13	12	sbcbii 3101	. 2 ⊢ ([̣A / x]̣[̣B / y]̣φ ↔ [̣A / x]̣∃y(y = B ∧ φ))
14		sbc5 3070	. . 3 ⊢ ([̣A / x]̣φ ↔ ∃x(x = A ∧ φ))
15	14	sbcbii 3101	. 2 ⊢ ([̣B / y]̣[̣A / x]̣φ ↔ [̣B / y]̣∃x(x = A ∧ φ))
16	11, 13, 15	3bitr4i 268	1 ⊢ ([̣A / x]̣[̣B / y]̣φ ↔ [̣B / y]̣[̣A / x]̣φ)

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642  [̣wsbc 3046

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-sbc 3047

This theorem is referenced by:  sbccom  3117