Theorem dfclel 2816

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815

This theorem is referenced by:  elex2  2817  issettru  2818  issetlem  2820  elissetv  2821  eleq1w  2823  eleq2w  2824  eleq1d  2825  eleq2d  2826  eleq2dALT  2827  clabel  2885  nfeld  2913  risset  3215  elexOLD  3454  elrabi  3632  sbcimdv  3798  sbcg  3802  sbcabel  3817  ssel  3916  noel  4273  disjsn  4650  pwpw0  4751  mptpreima  6196  fi1uzind  14467  brfi1indALT  14470  ballotlem2  34680  lfuhgr3  35355  eldm3  35996  mh-infprim3bi  36783  bj-dfsbc  36999  eliminable3a  37223  eliminable3b  37224  eliminable-abelv  37229  eliminable-abelab  37230  bj-denoteslem  37231  bj-issetwt  37235  bj-elsngl  37328  wl-dfcleq  37883  wl-dfclab  37963  chnsubseqword  47330