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 ⊢ A ∈ V ∧ B ∈ W → ∀ z ∀ w φ → z = A ∧ w = B ∧ [˙A / z]˙ [˙B / w]˙ φ ↔ ∀ z ∀ w φ → z = A ∧ w = B ∧ ∃ z ∃ w φ

Proof

Step Hyp Ref Expression
1 2sbc5g ⊢ A ∈ V ∧ B ∈ W → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ
2 1 adantr ⊢ A ∈ V ∧ B ∈ W ∧ ∀ z ∀ w φ → z = A ∧ w = B → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ
3 nfa1 ⊢ Ⅎ z ∀ z ∀ w φ → z = A ∧ w = B
4 nfa2 ⊢ Ⅎ w ∀ z ∀ w φ → z = A ∧ w = B
5 simpr ⊢ z = A ∧ w = B ∧ φ → φ
6 2sp ⊢ ∀ z ∀ w φ → z = A ∧ w = B → φ → z = A ∧ w = B
7 6 ancrd ⊢ ∀ z ∀ w φ → z = A ∧ w = B → φ → z = A ∧ w = B ∧ φ
8 5 7 impbid2 ⊢ ∀ z ∀ w φ → z = A ∧ w = B → z = A ∧ w = B ∧ φ ↔ φ
9 4 8 exbid ⊢ ∀ z ∀ w φ → z = A ∧ w = B → ∃ w z = A ∧ w = B ∧ φ ↔ ∃ w φ
10 3 9 exbid ⊢ ∀ z ∀ w φ → z = A ∧ w = B → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ ∃ z ∃ w φ
11 10 adantl ⊢ A ∈ V ∧ B ∈ W ∧ ∀ z ∀ w φ → z = A ∧ w = B → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ ∃ z ∃ w φ
12 2 11 bitr3d ⊢ A ∈ V ∧ B ∈ W ∧ ∀ z ∀ w φ → z = A ∧ w = B → [˙A / z]˙ [˙B / w]˙ φ ↔ ∃ z ∃ w φ
13 12 pm5.32da ⊢ A ∈ V ∧ B ∈ W → ∀ z ∀ w φ → z = A ∧ w = B ∧ [˙A / z]˙ [˙B / w]˙ φ ↔ ∀ z ∀ w φ → z = A ∧ w = B ∧ ∃ z ∃ w φ