Theorem cleljust 985

Description: When the class variables in definition df-clel 1099 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 803 with the class variables in wcel 1092.

Assertion

Ref	Expression
cleljust	⊢ (x ∈ y ↔ ∃z(z = x ∧ z ∈ y))

Distinct variable group(s):   x,z   y,z

Proof of Theorem cleljust

Step	Hyp	Ref	Expression
1		ax-17 925	. . 3 ⊢ (x ∈ y → ∀z x ∈ y)
2		a13b 819	. . 3 ⊢ (z = x → (z ∈ y ↔ x ∈ y))
3	1, 2	eqsex 834	. 2 ⊢ (∃z(z = x ∧ z ∈ y) ↔ x ∈ y)
4	3	bicomi 150	1 ⊢ (x ∈ y ↔ ∃z(z = x ∧ z ∈ y))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678   = weq 797   ∈ wel 803

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-13 804  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org