Metamath Proof Explorer


Theorem sbccom2lem

Description: Lemma for sbccom2 . (Contributed by Giovanni Mascellani, 31-May-2019)

Ref Expression
Hypothesis sbccom2lem.1
|- A e. _V
Assertion sbccom2lem
|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 sbccom2lem.1
 |-  A e. _V
2 sbcan
 |-  ( [. A / x ]. ( y = B /\ ph ) <-> ( [. A / x ]. y = B /\ [. A / x ]. ph ) )
3 sbc5
 |-  ( [. A / x ]. ( y = B /\ ph ) <-> E. x ( x = A /\ ( y = B /\ ph ) ) )
4 1 csbconstgi
 |-  [_ A / x ]_ y = y
5 eqid
 |-  [_ A / x ]_ B = [_ A / x ]_ B
6 1 4 5 sbceqi
 |-  ( [. A / x ]. y = B <-> y = [_ A / x ]_ B )
7 6 anbi1i
 |-  ( ( [. A / x ]. y = B /\ [. A / x ]. ph ) <-> ( y = [_ A / x ]_ B /\ [. A / x ]. ph ) )
8 2 3 7 3bitr3i
 |-  ( E. x ( x = A /\ ( y = B /\ ph ) ) <-> ( y = [_ A / x ]_ B /\ [. A / x ]. ph ) )
9 8 exbii
 |-  ( E. y E. x ( x = A /\ ( y = B /\ ph ) ) <-> E. y ( y = [_ A / x ]_ B /\ [. A / x ]. ph ) )
10 sbc5
 |-  ( [. B / y ]. ph <-> E. y ( y = B /\ ph ) )
11 10 sbcbii
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. A / x ]. E. y ( y = B /\ ph ) )
12 sbc5
 |-  ( [. A / x ]. E. y ( y = B /\ ph ) <-> E. x ( x = A /\ E. y ( y = B /\ ph ) ) )
13 11 12 bitri
 |-  ( [. A / x ]. [. B / y ]. ph <-> E. x ( x = A /\ E. y ( y = B /\ ph ) ) )
14 19.42v
 |-  ( E. y ( x = A /\ ( y = B /\ ph ) ) <-> ( x = A /\ E. y ( y = B /\ ph ) ) )
15 14 bicomi
 |-  ( ( x = A /\ E. y ( y = B /\ ph ) ) <-> E. y ( x = A /\ ( y = B /\ ph ) ) )
16 15 exbii
 |-  ( E. x ( x = A /\ E. y ( y = B /\ ph ) ) <-> E. x E. y ( x = A /\ ( y = B /\ ph ) ) )
17 excom
 |-  ( E. x E. y ( x = A /\ ( y = B /\ ph ) ) <-> E. y E. x ( x = A /\ ( y = B /\ ph ) ) )
18 16 17 bitri
 |-  ( E. x ( x = A /\ E. y ( y = B /\ ph ) ) <-> E. y E. x ( x = A /\ ( y = B /\ ph ) ) )
19 13 18 bitri
 |-  ( [. A / x ]. [. B / y ]. ph <-> E. y E. x ( x = A /\ ( y = B /\ ph ) ) )
20 sbc5
 |-  ( [. [_ A / x ]_ B / y ]. [. A / x ]. ph <-> E. y ( y = [_ A / x ]_ B /\ [. A / x ]. ph ) )
21 9 19 20 3bitr4i
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )