Theorem axext 1459

Description: The Axiom of Extensionality (ax-ext 1458) 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 1458	. 2 |- (A.z(z e. x <-> z e. y) -> x = y)
2		19.36v 1299	. 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 953   = wceq 955   e. wcel 957  E.wex 979

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-ext 1458

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

Copyright terms: Public domain