Theorem dfclel 2804

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 2803	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 2803

This theorem is referenced by:  elex2  2805  issettru  2806  issetlem  2808  elissetv  2809  eleq1w  2811  eleq2w  2812  eleq1d  2813  eleq2d  2814  eleq2dALT  2815  clabel  2874  nfeld  2903  risset  3212  elexOLD  3469  elrabi  3654  sbcimdv  3822  sbcg  3826  sbcabel  3841  ssel  3940  noel  4301  disjsn  4675  pwpw0  4777  mptpreima  6211  fi1uzind  14472  brfi1indALT  14475  ballotlem2  34480  lfuhgr3  35107  eldm3  35748  eliminable3a  36851  eliminable3b  36852  eliminable-abelv  36857  eliminable-abelab  36858  bj-denoteslem  36859  bj-issetwt  36863  bj-elsngl  36956  wl-dfclab  37584