Metamath Proof Explorer

Theorem 2sbc6g

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

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

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑤 = 𝑦 ↔ 𝑤 = 𝐵 ) )
2 1 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ) )
3 2 imbi1d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ) )
4 3 2albidv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ) )
5 dfsbcq ⊢ ( 𝑦 = 𝐵 → ( [ 𝑦 / 𝑤 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] 𝜑 ) )
6 5 sbcbidv ⊢ ( 𝑦 = 𝐵 → ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
7 4 6 bibi12d ⊢ ( 𝑦 = 𝐵 → ( ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ) )
8 eqeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝐴 ) )
9 8 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) ↔ ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) )
10 9 imbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ) )
11 10 2albidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ) )
12 dfsbcq ⊢ ( 𝑥 = 𝐴 → ( [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
13 11 12 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ↔ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ) )
14 vex ⊢ 𝑥 ∈ V
15 14 sbc6 ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 ↔ ∀ 𝑧 ( 𝑧 = 𝑥 → [ 𝑦 / 𝑤 ] 𝜑 ) )
16 19.21v ⊢ ( ∀ 𝑤 ( 𝑧 = 𝑥 → ( 𝑤 = 𝑦 → 𝜑 ) ) ↔ ( 𝑧 = 𝑥 → ∀ 𝑤 ( 𝑤 = 𝑦 → 𝜑 ) ) )
17 impexp ⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ ( 𝑧 = 𝑥 → ( 𝑤 = 𝑦 → 𝜑 ) ) )
18 17 albii ⊢ ( ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ ∀ 𝑤 ( 𝑧 = 𝑥 → ( 𝑤 = 𝑦 → 𝜑 ) ) )
19 vex ⊢ 𝑦 ∈ V
20 19 sbc6 ⊢ ( [ 𝑦 / 𝑤 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑦 → 𝜑 ) )
21 20 imbi2i ⊢ ( ( 𝑧 = 𝑥 → [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ( 𝑧 = 𝑥 → ∀ 𝑤 ( 𝑤 = 𝑦 → 𝜑 ) ) )
22 16 18 21 3bitr4ri ⊢ ( ( 𝑧 = 𝑥 → [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) )
23 22 albii ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → [ 𝑦 / 𝑤 ] 𝜑 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) )
24 15 23 bitr2i ⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → 𝜑 ) ↔ [ 𝑥 / 𝑧 ] [ 𝑦 / 𝑤 ] 𝜑 )
25 7 13 24 vtocl2g ⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
26 25 ancoms ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )