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

Theorem axext2 2386
Description: The Axiom of Extensionality (ax-ext 2385) 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 2385 . 2  |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
2 19.36v 1915 . 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 1662  ax-8 1683  ax-6 1740  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator