Theorem sbccomlem

Description: Lemma for sbccom . (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 18-Oct-2016)

	Ref	Expression
Assertion	sbccomlem	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
2		exdistr	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
3		an12	⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑦 = 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4	3	exbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝑦 = 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
5		19.42v	⊢ ( ∃ 𝑥 ( 𝑦 = 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑦 = 𝐵 ∧ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
6	4 5	bitri	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑦 = 𝐵 ∧ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
7	6	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
8	1 2 7	3bitr3i	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
9		sbc5	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
10		sbc5	⊢ ( [ 𝐵 / 𝑦 ] ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
11	8 9 10	3bitr4i	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ [ 𝐵 / 𝑦 ] ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
12		sbc5	⊢ ( [ 𝐵 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) )
13	12	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) )
14		sbc5	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
15	14	sbcbii	⊢ ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
16	11 13 15	3bitr4i	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )