Theorem risset 3210

Description: Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
risset	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem risset

Step	Hyp	Ref	Expression
1		exancom 1861	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2804	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 304	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

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

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  df-rex 3054

This theorem is referenced by:  nelb  3211  ceqsralv  3485  clel5  3628  reueq  3705  reuind  3721  0el  4322  iunidOLD  5020  reusv3  5355  elidinxp  6004  sucel  6396  fvmptt  6970  releldm2  8001  qsid  8731  ttrcltr  9645  zorng  10433  rereccl  11876  nndiv  12208  incexc2  15780  ruclem12  16185  conjnmzb  19161  pgpfac1lem2  19983  pgpfac1lem4  19986  mat1dimelbas  22334  mat1dimbas  22335  chmaidscmat  22711  unisngl  23390  fmid  23823  dcubic  26732  addsrid  27847  addsprop  27859  negsprop  27917  mulsrid  27992  mulsprop  28009  onsfi  28223  fusgrn0degnn0  29403  chscllem2  31540  disjunsn  32496  grplsm0l  33347  ballotlemsima  34480  dfon2lem8  35751  brimg  35898  dfrecs2  35911  altopelaltxp  35937  prtlem9  38830  prter2  38847  2llnmat  39491  2lnat  39751  cdlemefrs29bpre1  40364  elnn0rabdioph  42764  fiphp3d  42780  minregex  43496