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

Metamath Proof Explorer

Theorem sbal1

Description: Check out sbal for a version not dependent on ax-13 . A theorem used in elimination of disjoint variable restriction on x and z by replacing it with a distinctor -. A. x x = z . (Contributed by NM, 15-May-1993) (Proof shortened by Wolf Lammen, 3-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbal1 ⊢ ¬ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ

Proof

Step Hyp Ref Expression
1 sb4b ⊢ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ y y = z → ∀ x φ
2 nfnae ⊢ Ⅎ y ¬ ∀ x x = z
3 nfeqf2 ⊢ ¬ ∀ x x = z → Ⅎ x y = z
4 19.21t ⊢ Ⅎ x y = z → ∀ x y = z → φ ↔ y = z → ∀ x φ
5 4 bicomd ⊢ Ⅎ x y = z → y = z → ∀ x φ ↔ ∀ x y = z → φ
6 3 5 syl ⊢ ¬ ∀ x x = z → y = z → ∀ x φ ↔ ∀ x y = z → φ
7 2 6 albid ⊢ ¬ ∀ x x = z → ∀ y y = z → ∀ x φ ↔ ∀ y ∀ x y = z → φ
8 1 7 sylan9bbr ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ y ∀ x y = z → φ
9 nfnae ⊢ Ⅎ x ¬ ∀ y y = z
10 sb4b ⊢ ¬ ∀ y y = z → z y φ ↔ ∀ y y = z → φ
11 9 10 albid ⊢ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ x ∀ y y = z → φ
12 alcom ⊢ ∀ x ∀ y y = z → φ ↔ ∀ y ∀ x y = z → φ
13 11 12 bitrdi ⊢ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ y ∀ x y = z → φ
14 13 adantl ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ y ∀ x y = z → φ
15 8 14 bitr4d ⊢ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
16 15 ex ⊢ ¬ ∀ x x = z → ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
17 sbequ12 ⊢ y = z → ∀ x φ ↔ z y ∀ x φ
18 17 sps ⊢ ∀ y y = z → ∀ x φ ↔ z y ∀ x φ
19 sbequ12 ⊢ y = z → φ ↔ z y φ
20 19 sps ⊢ ∀ y y = z → φ ↔ z y φ
21 20 dral2 ⊢ ∀ y y = z → ∀ x φ ↔ ∀ x z y φ
22 18 21 bitr3d ⊢ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
23 16 22 pm2.61d2 ⊢ ¬ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ