Theorem axext 1453

Description: The Axiom of Extensionality (ax-ext 1452) 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.

Assertion

Ref	Expression
axext	|- E.z((z e. x <-> z e. y) -> x = y)

Distinct variable group:   x,y,z

Proof of Theorem axext

Step	Hyp	Ref	Expression
1		ax-ext 1452	. 2 |- (A.z(z e. x <-> z e. y) -> x = y)
2		19.36v 1295	. 2 |- (E.z((z e. x <-> z e. y) -> x = y) <-> (A.z(z e. x <-> z e. y) -> x = y))
3	1, 2	mpbir 190	1 |- E.z((z e. x <-> z e. y) -> x = y)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953   e. wcel 955  E.wex 977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain