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 )