Theorem sbccomieg

Description: Commute two explicit substitutions, using an implicit substitution to rewrite the exiting substitution. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	sbccomieg.1	⊢ ( 𝑎 = 𝐴 → 𝐵 = 𝐶 )
Assertion	sbccomieg	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 ↔ [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbccomieg.1	⊢ ( 𝑎 = 𝐴 → 𝐵 = 𝐶 )
2		sbcex	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 → 𝐴 ∈ V )
3		spesbc	⊢ ( [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 → ∃ 𝑏 [ 𝐴 / 𝑎 ] 𝜑 )
4		sbcex	⊢ ( [ 𝐴 / 𝑎 ] 𝜑 → 𝐴 ∈ V )
5	4	exlimiv	⊢ ( ∃ 𝑏 [ 𝐴 / 𝑎 ] 𝜑 → 𝐴 ∈ V )
6	3 5	syl	⊢ ( [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 → 𝐴 ∈ V )
7		nfcv	⊢ Ⅎ 𝑎 𝐶
8		nfsbc1v	⊢ Ⅎ 𝑎 [ 𝐴 / 𝑎 ] 𝜑
9	7 8	nfsbcw	⊢ Ⅎ 𝑎 [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑
10		sbceq1a	⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑎 ] 𝜑 ) )
11	1 10	sbceqbid	⊢ ( 𝑎 = 𝐴 → ( [ 𝐵 / 𝑏 ] 𝜑 ↔ [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 ) )
12	9 11	sbciegf	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 ↔ [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 ) )
13	2 6 12	pm5.21nii	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 ↔ [ 𝐶 / 𝑏 ] [ 𝐴 / 𝑎 ] 𝜑 )