Theorem dfclel 2807

Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.)

Assertion

Ref	Expression
dfclel	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfclel

Dummy variables 𝑦 𝑧 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cleljust 2120	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2120	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2806	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806

This theorem is referenced by:  elex2  2808  issettru  2809  issetlem  2811  elissetv  2812  eleq1w  2814  eleq2w  2815  eleq1d  2816  eleq2d  2817  eleq2dALT  2818  clabel  2877  nfeld  2906  risset  3207  elexOLD  3458  elrabi  3643  sbcimdv  3810  sbcg  3814  sbcabel  3829  ssel  3928  noel  4288  disjsn  4664  pwpw0  4765  mptpreima  6185  fi1uzind  14411  brfi1indALT  14414  ballotlem2  34497  lfuhgr3  35152  eldm3  35793  eliminable3a  36896  eliminable3b  36897  eliminable-abelv  36902  eliminable-abelab  36903  bj-denoteslem  36904  bj-issetwt  36908  bj-elsngl  37001  wl-dfclab  37629