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

Theorem axext2 1878
Description: The Axiom of Extensionality (ax-ext 1877) 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.
Assertion
Ref Expression
axext2
Distinct variable group:   ,,

Proof of Theorem axext2
StepHypRef Expression
1 ax-ext 1877 . 2
2 19.36v 1701 . 2
31, 2mpbir 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 173  wal 1322  wex 1327   wceq 1398   wcel 1400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-gen 1326  ax-17 1413  ax-4 1429  ax-ext 1877
This theorem depends on definitions:  df-bi 174  df-an 357  df-ex 1328
  Copyright terms: Public domain W3C validator