Theorem risset 3267

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 3144	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2894	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 306	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893  df-rex 3144

This theorem is referenced by:  nelb  3268  clel5  3657  reueq  3728  reuind  3744  0el  4320  iunid  4984  reusv3  5306  elidinxp  5911  sucel  6264  fvmptt  6788  releldm2  7742  qsid  8363  zorng  9926  rereccl  11358  nndiv  11684  incexc2  15193  ruclem12  15594  conjnmzb  18393  pgpfac1lem2  19197  pgpfac1lem4  19200  mat1dimelbas  21080  mat1dimbas  21081  chmaidscmat  21456  unisngl  22135  fmid  22568  dcubic  25424  fusgrn0degnn0  27281  chscllem2  29415  disjunsn  30344  ballotlemsima  31773  dfon2lem8  33035  brimg  33398  dfrecs2  33411  altopelaltxp  33437  prtlem9  36015  prter2  36032  2llnmat  36675  2lnat  36935  cdlemefrs29bpre1  37548  elnn0rabdioph  39420  fiphp3d  39436