Metamath Proof Explorer

Theorem wl-ax11-lem10

Description: We now have prepared everything. The unwanted variable u is just in one place left. pm2.61 can be used in conjunction with wl-ax11-lem9 to eliminate the second antecedent. Missing is something along the lines of ax-6 , so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem10 ⊢ ∀ y y = u → ¬ ∀ x x = y → ∀ y ∀ x φ → ∀ x ∀ y φ

Proof

Step Hyp Ref Expression
1 wl-ax11-lem8 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ y ∀ x φ
2 wl-ax11-lem6 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ x ∀ y φ
3 1 2 bitr3d ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ y ∀ x φ ↔ ∀ x ∀ y φ
4 3 biimpd ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ y ∀ x φ → ∀ x ∀ y φ
5 4 ex ⊢ ∀ u u = y → ¬ ∀ x x = y → ∀ y ∀ x φ → ∀ x ∀ y φ
6 5 aecoms ⊢ ∀ y y = u → ¬ ∀ x x = y → ∀ y ∀ x φ → ∀ x ∀ y φ