Theorem dfclel 2805

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804

This theorem is referenced by:  elex2  2806  issettru  2807  issetlem  2809  elissetv  2810  eleq1w  2812  eleq2w  2813  eleq1d  2814  eleq2d  2815  eleq2dALT  2816  clabel  2875  nfeld  2904  risset  3213  elexOLD  3472  elrabi  3657  sbcimdv  3825  sbcg  3829  sbcabel  3844  ssel  3943  noel  4304  disjsn  4678  pwpw0  4780  mptpreima  6214  fi1uzind  14479  brfi1indALT  14482  ballotlem2  34487  lfuhgr3  35114  eldm3  35755  eliminable3a  36858  eliminable3b  36859  eliminable-abelv  36864  eliminable-abelab  36865  bj-denoteslem  36866  bj-issetwt  36870  bj-elsngl  36963  wl-dfclab  37591