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 ) |