Metamath Proof Explorer

Theorem wl-2sb6d

Description: Version of 2sb6 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019)

Ref Expression
Hypotheses wl-2sb6d.1 ⊢ φ → ¬ ∀ y y = x
wl-2sb6d.2 ⊢ φ → ¬ ∀ y y = w
wl-2sb6d.3 ⊢ φ → ¬ ∀ y y = z
wl-2sb6d.4 ⊢ φ → ¬ ∀ x x = z
Assertion wl-2sb6d ⊢ φ → z x w y ψ ↔ ∀ x ∀ y x = z ∧ y = w → ψ

Proof

Step Hyp Ref Expression
1 wl-2sb6d.1 ⊢ φ → ¬ ∀ y y = x
2 wl-2sb6d.2 ⊢ φ → ¬ ∀ y y = w
3 wl-2sb6d.3 ⊢ φ → ¬ ∀ y y = z
4 wl-2sb6d.4 ⊢ φ → ¬ ∀ x x = z
5 1 3 jca ⊢ φ → ¬ ∀ y y = x ∧ ¬ ∀ y y = z
6 sb4b ⊢ ¬ ∀ x x = z → z x w y ψ ↔ ∀ x x = z → w y ψ
7 nfnae ⊢ Ⅎ x ¬ ∀ y y = w
8 wl-nfnae1 ⊢ Ⅎ x ¬ ∀ y y = x
9 nfnae ⊢ Ⅎ x ¬ ∀ y y = z
10 8 9 nfan ⊢ Ⅎ x ¬ ∀ y y = x ∧ ¬ ∀ y y = z
11 7 10 nfan ⊢ Ⅎ x ¬ ∀ y y = w ∧ ¬ ∀ y y = x ∧ ¬ ∀ y y = z
12 sb4b ⊢ ¬ ∀ y y = w → w y ψ ↔ ∀ y y = w → ψ
13 12 imbi2d ⊢ ¬ ∀ y y = w → x = z → w y ψ ↔ x = z → ∀ y y = w → ψ
14 impexp ⊢ x = z ∧ y = w → ψ ↔ x = z → y = w → ψ
15 14 albii ⊢ ∀ y x = z ∧ y = w → ψ ↔ ∀ y x = z → y = w → ψ
16 nfeqf ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y x = z
17 19.21t ⊢ Ⅎ y x = z → ∀ y x = z → y = w → ψ ↔ x = z → ∀ y y = w → ψ
18 16 17 syl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ y x = z → y = w → ψ ↔ x = z → ∀ y y = w → ψ
19 15 18 bitr2id ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → x = z → ∀ y y = w → ψ ↔ ∀ y x = z ∧ y = w → ψ
20 13 19 sylan9bb ⊢ ¬ ∀ y y = w ∧ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → x = z → w y ψ ↔ ∀ y x = z ∧ y = w → ψ
21 11 20 albid ⊢ ¬ ∀ y y = w ∧ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ x x = z → w y ψ ↔ ∀ x ∀ y x = z ∧ y = w → ψ
22 6 21 sylan9bb ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = w ∧ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → z x w y ψ ↔ ∀ x ∀ y x = z ∧ y = w → ψ
23 4 2 5 22 syl12anc ⊢ φ → z x w y ψ ↔ ∀ x ∀ y x = z ∧ y = w → ψ