Theorem sbccom2fi

Description: Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019)

	Ref	Expression
Hypotheses	sbccom2fi.1	⊢ 𝐴 ∈ V
	sbccom2fi.2	⊢ Ⅎ 𝑦 𝐴
	sbccom2fi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶
	sbccom2fi.4	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
Assertion	sbccom2fi	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐶 / 𝑦 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbccom2fi.1	⊢ 𝐴 ∈ V
2		sbccom2fi.2	⊢ Ⅎ 𝑦 𝐴
3		sbccom2fi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶
4		sbccom2fi.4	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
5	1 2	sbccom2f	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
6		dfsbcq	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 → ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
7	3 6	ax-mp	⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
8	4	sbcbii	⊢ ( [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐶 / 𝑦 ] 𝜓 )
9	5 7 8	3bitri	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐶 / 𝑦 ] 𝜓 )