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

Metamath Proof Explorer

Theorem ax11w

Description: Weak version of ax-11 from which we can prove any ax-11 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. Unlike ax-11 , this theorem requires that x and y be distinct i.e. are not bundled. It is an alias of alcomimw introduced for labeling consistency. (Contributed by NM, 10-Apr-2017) Use alcomimw instead. (New usage is discouraged.)

Ref Expression
Hypothesis ax11w.1 ⊢ y = z → φ ↔ ψ
Assertion ax11w ⊢ ∀ x ∀ y φ → ∀ y ∀ x φ

Proof

Step Hyp Ref Expression
1 ax11w.1 ⊢ y = z → φ ↔ ψ
2 1 alcomimw ⊢ ∀ x ∀ y φ → ∀ y ∀ x φ