Metamath Proof Explorer

Theorem 2sbc5g

Description: Theorem *13.22 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011)

Ref Expression
Assertion 2sbc5g ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑤 = 𝑦 ↔ 𝑤 = 𝐵 ) )
2 1 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ) )
3 2 anbi1d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ) )
4 3 2exbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ) )
5 dfsbcq ⊢ ( 𝑦 = 𝐵 → ( [ 𝑦 / 𝑤 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] 𝜑 ) )
6 5 sbcbidv ⊢ ( 𝑦 = 𝐵 → ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
7 4 6 bibi12d ⊢ ( 𝑦 = 𝐵 → ( ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ) )
8 eqeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝐴 ) )
9 8 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ↔ ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) )
10 9 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ) )
11 10 2exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ) )
12 dfsbcq ⊢ ( 𝑥 = 𝐴 → ( [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
13 11 12 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ↔ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ) )
14 sbc5 ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ [ 𝑦 / 𝑤 ] 𝜑 ) )
15 19.42v ⊢ ( ∃ 𝑤 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
16 anass ⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
17 16 exbii ⊢ ( ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑤 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
18 sbc5 ⊢ ( [ 𝑦 / 𝑤 ] 𝜑 ↔ ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝜑 ) )
19 18 anbi2i ⊢ ( ( 𝑧 = 𝑥 ∧ [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
20 15 17 19 3bitr4ri ⊢ ( ( 𝑧 = 𝑥 ∧ [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
21 20 exbii ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
22 14 21 bitr2i ⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 )
23 7 13 22 vtocl2g ⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
24 23 ancoms ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )