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

Theorem axext2 2235
Description: The Axiom of Extensionality (ax-ext 2234) 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 2234 . 2  |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
2 19.36v 2029 . 2  |-  ( E. z ( ( z  e.  x  <->  z  e.  y )  ->  x  =  y )  <->  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y ) )
31, 2mpbir 202 1  |-  E. z
( ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator