MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axext2 Unicode version

Theorem axext2 2371
Description: The Axiom of Extensionality (ax-ext 2370) restated so that it postulates the existence of a set  z given two arbitrary sets 
x and  y. This way to express it follows the general idea of the other ZFC axioms, which is to postulate the existence of sets given other sets. (Contributed by NM, 28-Sep-2003.)
Assertion
Ref Expression
axext2  |-  E. z
( ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
Distinct variable group:    x, y, z

Proof of Theorem axext2
StepHypRef Expression
1 ax-ext 2370 . 2  |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
2 19.36v 1908 . 2  |-  ( E. z ( ( z  e.  x  <->  z  e.  y )  ->  x  =  y )  <->  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y ) )
31, 2mpbir 201 1  |-  E. z
( ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   E.wex 1547
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator