Theorem cleljust 2014

Description: When the class variables in definition df-clel 2349 are replaced with setvar 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 setvar variables in wel 1711 with the class variables in wcel 1710. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.)

Assertion

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

Distinct variable groups:   x,z   y,z

Proof of Theorem cleljust

Step	Hyp	Ref	Expression
1		ax-17 1616	. . 3 ⊢ (x ∈ y → ∀z x ∈ y)
2		elequ1 1713	. . 3 ⊢ (z = x → (z ∈ y ↔ x ∈ y))
3	1, 2	equsexh 1963	. 2 ⊢ (∃z(z = x ∧ z ∈ y) ↔ x ∈ y)
4	3	bicomi 193	1 ⊢ (x ∈ y ↔ ∃z(z = x ∧ z ∈ y))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by: (None)