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	⊢ 𝐴 ∈ V
	sbccom2f.2	⊢ Ⅎ 𝑦 𝐴
Assertion	sbccom2f	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbccom2f.1	⊢ 𝐴 ∈ V
2		sbccom2f.2	⊢ Ⅎ 𝑦 𝐴
3		sbcco	⊢ ( [ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜑 )
4	3	bicomi	⊢ ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜑 )
5	4	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜑 )
6	1	sbccom2	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑧 ] [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
7		vex	⊢ 𝑧 ∈ V
8	7	sbccom2	⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
9	7 2	csbgfi	⊢ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 = 𝐴
10		dfsbcq	⊢ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 = 𝐴 → ( [ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ) )
11	9 10	ax-mp	⊢ ( [ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
12	8 11	bitri	⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
13	12	bicomi	⊢ ( [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
14	13	sbcbii	⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑧 ] [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
15		sbcco	⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑧 ] [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
16	14 15	bitri	⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑧 ] [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
17	5 6 16	3bitri	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )