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 ⊢φ→¬∀yy=x
wl-2sb6d.2 ⊢φ→¬∀yy=w
wl-2sb6d.3 ⊢φ→¬∀yy=z
wl-2sb6d.4 ⊢φ→¬∀xx=z
Assertion wl-2sb6d ⊢φ→zxwyψ↔∀x∀yx=z∧y=w→ψ

Proof

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