Metamath Proof Explorer

Theorem sbccomlem

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

Ref Expression
Assertion sbccomlem 
|- ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 excom 
 |-  ( E. x E. y ( x = A /\ ( y = B /\ ph ) ) <-> E. y E. x ( x = A /\ ( y = B /\ ph ) ) )
2 exdistr 
 |-  ( E. x E. y ( x = A /\ ( y = B /\ ph ) ) <-> E. x ( x = A /\ E. y ( y = B /\ ph ) ) )
3 an12 
 |-  ( ( x = A /\ ( y = B /\ ph ) ) <-> ( y = B /\ ( x = A /\ ph ) ) )
4 3 exbii 
 |-  ( E. x ( x = A /\ ( y = B /\ ph ) ) <-> E. x ( y = B /\ ( x = A /\ ph ) ) )
5 19.42v 
 |-  ( E. x ( y = B /\ ( x = A /\ ph ) ) <-> ( y = B /\ E. x ( x = A /\ ph ) ) )
6 4 5 bitri 
 |-  ( E. x ( x = A /\ ( y = B /\ ph ) ) <-> ( y = B /\ E. x ( x = A /\ ph ) ) )
7 6 exbii 
 |-  ( E. y E. x ( x = A /\ ( y = B /\ ph ) ) <-> E. y ( y = B /\ E. x ( x = A /\ ph ) ) )
8 1 2 7 3bitr3i 
 |-  ( E. x ( x = A /\ E. y ( y = B /\ ph ) ) <-> E. y ( y = B /\ E. x ( x = A /\ ph ) ) )
9 sbc5 
 |-  ( [. A / x ]. E. y ( y = B /\ ph ) <-> E. x ( x = A /\ E. y ( y = B /\ ph ) ) )
10 sbc5 
 |-  ( [. B / y ]. E. x ( x = A /\ ph ) <-> E. y ( y = B /\ E. x ( x = A /\ ph ) ) )
11 8 9 10 3bitr4i 
 |-  ( [. A / x ]. E. y ( y = B /\ ph ) <-> [. B / y ]. E. x ( x = A /\ ph ) )
12 sbc5 
 |-  ( [. B / y ]. ph <-> E. y ( y = B /\ ph ) )
13 12 sbcbii 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. A / x ]. E. y ( y = B /\ ph ) )
14 sbc5 
 |-  ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )
15 14 sbcbii 
 |-  ( [. B / y ]. [. A / x ]. ph <-> [. B / y ]. E. x ( x = A /\ ph ) )
16 11 13 15 3bitr4i 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph )