Theorem dfclel 2817

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

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

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 2007  ax-8 2110

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

This theorem is referenced by:  elex2  2818  issettru  2819  issetlem  2821  elissetv  2822  eleq1w  2824  eleq2w  2825  eleq1d  2826  eleq2d  2827  eleq2dALT  2828  clabel  2888  nfeld  2917  risset  3233  elexOLD  3502  elrabi  3687  sbcimdv  3859  sbcg  3863  sbcabel  3878  ssel  3977  noel  4338  disjsn  4711  pwpw0  4813  mptpreima  6258  fi1uzind  14546  brfi1indALT  14549  ballotlem2  34491  lfuhgr3  35125  eldm3  35761  eliminable3a  36864  eliminable3b  36865  eliminable-abelv  36870  eliminable-abelab  36871  bj-denoteslem  36872  bj-issetwt  36876  bj-elsngl  36969  wl-dfclab  37597