MPE Home 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  z is distinct from  x and  y, and  x  =  y is true, then  x  =  y quantified with  z is also true. In other words,  z is irrelevant to the truth of 
x  =  y. 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 2105, has been shown to be redundant (theorem ax15 2104).

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 1882 shows the reverse derivation. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-12o  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )

Detailed syntax breakdown of Axiom ax-12o
StepHypRef Expression
1 vz . . . . 5  set  z
2 vx . . . . 5  set  x
31, 2weq 1620 . . . 4  wff  z  =  x
43, 1wal 1532 . . 3  wff  A. z 
z  =  x
54wn 5 . 2  wff  -.  A. z  z  =  x
6 vy . . . . . 6  set  y
71, 6weq 1620 . . . . 5  wff  z  =  y
87, 1wal 1532 . . . 4  wff  A. z 
z  =  y
98wn 5 . . 3  wff  -.  A. z  z  =  y
102, 6weq 1620 . . . 4  wff  x  =  y
1110, 1wal 1532 . . . 4  wff  A. z  x  =  y
1210, 11wi 6 . . 3  wff  ( x  =  y  ->  A. z  x  =  y )
139, 12wi 6 . 2  wff  ( -. 
A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
)
145, 13wi 6 1  wff  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )
Colors of variables: wff set class
This axiom is referenced by:  hbequid  1687  equid  1818  equidALT  1819  hbae  1841  hbae-o  1842  nfeqf  1849  dvelimfALT  1854  dvelimf-o  1855  ax12  1882  ax17eq  1928  dvelimf  1976  dvelimALT  2097  ax11eq  2108  ax11indalem  2113  axext4dist  23512  ax12-2  28254  ax12-4  28257  ax10lem17ALT  28274  a12stdy4  28280  a12lem1  28281  ax9lem17  28307
  Copyright terms: Public domain W3C validator