Theorem dfclel 2815

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 2115	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2115	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2814	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814

This theorem is referenced by:  elex2  2816  issettru  2817  issetlem  2819  elissetv  2820  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2d  2825  eleq2dALT  2826  clabel  2886  nfeld  2915  risset  3231  elexOLD  3500  elrabi  3690  sbcimdv  3865  sbcg  3870  sbcabel  3887  ssel  3989  noel  4344  disjsn  4716  pwpw0  4818  mptpreima  6260  fi1uzind  14543  brfi1indALT  14546  ballotlem2  34470  lfuhgr3  35104  eldm3  35741  eliminable3a  36846  eliminable3b  36847  eliminable-abelv  36852  eliminable-abelab  36853  bj-denoteslem  36854  bj-issetwt  36858  bj-elsngl  36951  wl-dfclab  37577