Theorem cleljust 1330

Description: When the class variables in definition df-clel 1475 are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 961 with the class variables in wcel 960.

Assertion

Ref	Expression
cleljust	|- (x e. y <-> E.z(z = x /\ z e. y))

Distinct variable groups:   x,z   y,z

Proof of Theorem cleljust

Step	Hyp	Ref	Expression
1		ax-17 973	. . 3 |- (x e. y -> A.z x e. y)
2		elequ1 1138	. . 3 |- (z = x -> (z e. y <-> x e. y))
3	1, 2	equsex 1154	. 2 |- (E.z(z = x /\ z e. y) <-> x e. y)
4	3	bicomi 172	1 |- (x e. y <-> E.z(z = x /\ z e. y))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-8 966  ax-12 970  ax-13 971  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

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

Copyright terms: Public domain