This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm14.123b

Description: Theorem *14.123 in WhiteheadRussell p. 185. (Contributed by Andrew Salmon, 9-Jun-2011)

Ref Expression
Assertion pm14.123b ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ∧ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ↔ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ∧ ∃ 𝑧 ∃ 𝑤 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 2sbc5g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) )
3 nfa1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) )
4 nfa2 ⊢ Ⅎ 𝑤 ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) )
5 simpr ⊢ ( ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) → 𝜑 )
6 2sp ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) → ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) )
7 6 ancrd ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) → ( 𝜑 → ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ) )
8 5 7 impbid2 ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) → ( ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ 𝜑 ) )
9 4 8 exbid ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) → ( ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑤 𝜑 ) )
10 3 9 exbid ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 𝜑 ) )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ) → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 𝜑 ) )
12 2 11 bitr3d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ) → ( [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜑 ) )
13 12 pm5.32da ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ∧ [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] 𝜑 ) ↔ ( ∀ 𝑧 ∀ 𝑤 ( 𝜑 → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ) ∧ ∃ 𝑧 ∃ 𝑤 𝜑 ) ) )