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

Axiom ax-12o 1664
 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. The analogous axiom for the membership connective, ax-15 2102, has been shown to be redundant (theorem ax15 2101). In December 2015, this axiom was replaced with a shorter version, ax-12 1633. Theorem ax12o 1663 shows the derivation of ax-12o 1664 from ax-12 1633, and theorem ax12 1881 shows the reverse derivation. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-12o

Detailed syntax breakdown of Axiom ax-12o
StepHypRef Expression
1 vz . . . . 5
2 vx . . . . 5
31, 2weq 1620 . . . 4
43, 1wal 1532 . . 3
54wn 5 . 2
6 vy . . . . . 6
71, 6weq 1620 . . . . 5
87, 1wal 1532 . . . 4
98wn 5 . . 3
102, 6weq 1620 . . . 4
1110, 1wal 1532 . . . 4
1210, 11wi 6 . . 3
139, 12wi 6 . 2
145, 13wi 6 1
 Colors of variables: wff set class This axiom is referenced by:  hbequid  1687  equid  1818  equidALT  1819  hbae  1840  hbae-o  1841  nfeqf  1848  dvelimfALT  1853  dvelimf-o  1854  ax12  1881  ax17eq  1927  dvelimf  1975  dvelimALT  2094  ax11eq  2105  ax11indalem  2110  axext4dist  23325  ax12-2  27792  ax12-4  27795  ax10lem17ALT  27812  a12stdy4  27818  a12lem1  27819  ax9lem17  27845
 Copyright terms: Public domain W3C validator