Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-12o Structured version   Unicode version

Axiom ax-12o 2219
 Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever is distinct from and , and is true, then quantified with is also true. In other words, is irrelevant to the truth of . Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. This axiom is obsolete and should no longer be used. It is proved above as theorem ax12o 2010. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
Assertion
Ref Expression
ax-12o

Detailed syntax breakdown of Axiom ax-12o
StepHypRef Expression
1 vz . . . . 5
2 vx . . . . 5
31, 2weq 1653 . . . 4
43, 1wal 1549 . . 3
54wn 3 . 2
6 vy . . . . . 6
71, 6weq 1653 . . . . 5
87, 1wal 1549 . . . 4
98wn 3 . . 3
102, 6weq 1653 . . . 4
1110, 1wal 1549 . . . 4
1210, 11wi 4 . . 3
139, 12wi 4 . 2
145, 13wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  hbae-o  2230  ax12from12o  2233  equid1  2235  hbequid  2237  equid1ALT  2253  dvelimf-o  2257  ax17eq  2260
 Copyright terms: Public domain W3C validator