Metamath Proof Explorer

Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimf-o.1 ⊢φ→∀xφ
dvelimf-o.2 ⊢ψ→∀zψ
dvelimf-o.3 ⊢z=y→φ↔ψ
Assertion dvelimf-o ⊢¬∀xx=y→ψ→∀xψ

Proof

Step Hyp Ref Expression
1 dvelimf-o.1 ⊢φ→∀xφ
2 dvelimf-o.2 ⊢ψ→∀zψ
3 dvelimf-o.3 ⊢z=y→φ↔ψ
4 hba1-o ⊢∀zz=y→φ→∀z∀zz=y→φ
5 ax-c11 ⊢∀zz=x→∀z∀zz=y→φ→∀x∀zz=y→φ
6 5 aecoms-o ⊢∀xx=z→∀z∀zz=y→φ→∀x∀zz=y→φ
7 4 6 syl5 ⊢∀xx=z→∀zz=y→φ→∀x∀zz=y→φ
8 7 a1d ⊢∀xx=z→¬∀xx=y→∀zz=y→φ→∀x∀zz=y→φ
9 hbnae-o ⊢¬∀xx=z→∀z¬∀xx=z
10 hbnae-o ⊢¬∀xx=y→∀z¬∀xx=y
11 9 10 hban ⊢¬∀xx=z∧¬∀xx=y→∀z¬∀xx=z∧¬∀xx=y
12 hbnae-o ⊢¬∀xx=z→∀x¬∀xx=z
13 hbnae-o ⊢¬∀xx=y→∀x¬∀xx=y
14 12 13 hban ⊢¬∀xx=z∧¬∀xx=y→∀x¬∀xx=z∧¬∀xx=y
15 ax-c9 ⊢¬∀xx=z→¬∀xx=y→z=y→∀xz=y
16 15 imp ⊢¬∀xx=z∧¬∀xx=y→z=y→∀xz=y
17 1 a1i ⊢¬∀xx=z∧¬∀xx=y→φ→∀xφ
18 14 16 17 hbimd ⊢¬∀xx=z∧¬∀xx=y→z=y→φ→∀xz=y→φ
19 11 18 hbald ⊢¬∀xx=z∧¬∀xx=y→∀zz=y→φ→∀x∀zz=y→φ
20 19 ex ⊢¬∀xx=z→¬∀xx=y→∀zz=y→φ→∀x∀zz=y→φ
21 8 20 pm2.61i ⊢¬∀xx=y→∀zz=y→φ→∀x∀zz=y→φ
22 2 3 equsalh ⊢∀zz=y→φ↔ψ
23 22 albii ⊢∀x∀zz=y→φ↔∀xψ
24 21 22 23 3imtr3g ⊢¬∀xx=y→ψ→∀xψ