Theorem cleljustALT 2015

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. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) (Revised by Mario Carneiro, 21-Dec-2016.)

Assertion

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

Distinct variable groups:   x,z   y,z

Proof of Theorem cleljustALT

Step	Hyp	Ref	Expression
1		nfv 1619	. . 3 ⊢ Ⅎz x ∈ y
2		elequ1 1713	. . 3 ⊢ (z = x → (z ∈ y ↔ x ∈ y))
3	1, 2	equsex 1962	. 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)