# 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 ( ( 𝐴𝐶𝐵𝐷 ) → ( ∀ 𝑧𝑤 ( ( 𝑧 = 𝐴𝑤 = 𝐵 ) → 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )