Theorem sbccom2f

Description: Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypotheses	sbccom2f.1	|- A e. _V
	sbccom2f.2	|- F/_ y A
Assertion	sbccom2f	|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbccom2f.1	|- A e. _V
2		sbccom2f.2	|- F/_ y A
3		sbccow	|- ( [. B / z ]. [. z / y ]. ph <-> [. B / y ]. ph )
4	3	bicomi	|- ( [. B / y ]. ph <-> [. B / z ]. [. z / y ]. ph )
5	4	sbcbii	|- ( [. A / x ]. [. B / y ]. ph <-> [. A / x ]. [. B / z ]. [. z / y ]. ph )
6	1	sbccom2	|- ( [. A / x ]. [. B / z ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph )
7		vex	|- z e. _V
8	7	sbccom2	|- ( [. z / y ]. [. A / x ]. ph <-> [. [_ z / y ]_ A / x ]. [. z / y ]. ph )
9	7 2	csbgfi	|- [_ z / y ]_ A = A
10		dfsbcq	|- ( [_ z / y ]_ A = A -> ( [. [_ z / y ]_ A / x ]. [. z / y ]. ph <-> [. A / x ]. [. z / y ]. ph ) )
11	9 10	ax-mp	|- ( [. [_ z / y ]_ A / x ]. [. z / y ]. ph <-> [. A / x ]. [. z / y ]. ph )
12	8 11	bitri	|- ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. [. z / y ]. ph )
13	12	bicomi	|- ( [. A / x ]. [. z / y ]. ph <-> [. z / y ]. [. A / x ]. ph )
14	13	sbcbii	|- ( [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / z ]. [. z / y ]. [. A / x ]. ph )
15		sbccow	|- ( [. [_ A / x ]_ B / z ]. [. z / y ]. [. A / x ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
16	14 15	bitri	|- ( [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
17	5 6 16	3bitri	|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )