Theorem dfclel 2807

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-clel 2806

This theorem is referenced by:  elex2  2808  issetlem  2809  elissetv  2810  eleq1w  2812  eleq2w  2813  eleq1d  2814  eleq2d  2815  eleq2dALT  2816  clelabOLD  2876  clabel  2877  nfeld  2910  risset  3226  elex  3489  elrabi  3675  sbcimdv  3848  sbcg  3853  sbcabel  3869  ssel  3972  sselOLD  3973  noel  4327  noelOLD  4328  disjsn  4712  pwpw0  4813  mptpreima  6237  fi1uzind  14485  brfi1indALT  14488  ballotlem2  34103  lfuhgr3  34724  eldm3  35350  eliminable3a  36335  eliminable3b  36336  eliminable-abelv  36341  eliminable-abelab  36342  bj-denoteslem  36343  bj-issetwt  36347  bj-elsngl  36442  wl-dfclab  37058

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »