Theorem sbccom2lem

Description: Lemma for sbccom2 . (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypothesis	sbccom2lem.1	⊢ 𝐴 ∈ V
Assertion	sbccom2lem	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbccom2lem.1	⊢ 𝐴 ∈ V
2		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
3		sbc5	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
4	1	csbconstgi	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦
5		eqid	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵
6	1 4 5	sbceqi	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 ↔ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
7	6	anbi1i	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
8	2 3 7	3bitr3i	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
10		sbc5	⊢ ( [ 𝐵 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) )
11	10	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) )
12		sbc5	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
13	11 12	bitri	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
14		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
15	14	bicomi	⊢ ( ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
16	15	exbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
17		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
18	16 17	bitri	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
19	13 18	bitri	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝜑 ) ) )
20		sbc5	⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
21	9 19 20	3bitr4i	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )