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

Theorem axext2 2804
Description: The Axiom of Extensionality (ax-ext 2803) restated so that it postulates the existence of a set 𝑧 given two arbitrary sets 𝑥 and 𝑦. 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 𝑧((𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Distinct variable group:   𝑥,𝑦,𝑧

Proof of Theorem axext2
StepHypRef Expression
1 ax-ext 2803 . 2 (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
2 19.36v 2091 . 2 (∃𝑧((𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦) ↔ (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦))
31, 2mpbir 223 1 𝑧((𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1654  wex 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-ex 1879
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator