NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  axext2 GIF version

Theorem axext2 2335
Description: The Axiom of Extensionality (ax-ext 2334) 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 z((z xz y) → x = y)
Distinct variable group:   x,y,z

Proof of Theorem axext2
StepHypRef Expression
1 ax-ext 2334 . 2 (z(z xz y) → x = y)
2 19.36v 1896 . 2 (z((z xz y) → x = y) ↔ (z(z xz y) → x = y))
31, 2mpbir 200 1 z((z xz y) → x = y)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  wal 1540  wex 1541   = wceq 1642   wcel 1710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator