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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  elex2  2818  elissetv  2819  elisset  2820  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2d  2824  eleq2dALT  2825  clelabOLD  2884  clabel  2885  nfeld  2918  risset  3194  isset  3445  elex  3450  elrabi  3618  sbcimdv  3790  sbcg  3795  sbcabel  3811  ssel  3914  sselOLD  3915  noel  4264  noelOLD  4265  disjsn  4647  pwpw0  4746  pwsnOLD  4832  mptpreima  6141  fi1uzind  14211  brfi1indALT  14214  nelbOLDOLD  30817  ballotlem2  32455  lfuhgr3  33081  eldm3  33728  eliminable3a  35047  eliminable3b  35048  eliminable-abelv  35053  eliminable-abelab  35054  bj-denoteslem  35055  bj-issetwt  35059  bj-elsngl  35158  wl-dfclab  35747