Theorem risset 3193

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 1865	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2818	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 303	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817  df-rex 3069

This theorem is referenced by:  nelb  3194  nelbOLD  3195  ceqsralv  3459  clel5  3589  reueq  3667  reuind  3683  0el  4291  iunid  4986  reusv3  5323  elidinxp  5940  sucel  6324  fvmptt  6877  releldm2  7857  qsid  8530  zorng  10191  rereccl  11623  nndiv  11949  incexc2  15478  ruclem12  15878  conjnmzb  18784  pgpfac1lem2  19593  pgpfac1lem4  19596  mat1dimelbas  21528  mat1dimbas  21529  chmaidscmat  21905  unisngl  22586  fmid  23019  dcubic  25901  fusgrn0degnn0  27769  chscllem2  29901  disjunsn  30834  grplsm0l  31493  ballotlemsima  32382  dfon2lem8  33672  ttrcltr  33702  addsid1  34054  brimg  34166  dfrecs2  34179  altopelaltxp  34205  prtlem9  36805  prter2  36822  2llnmat  37465  2lnat  37725  cdlemefrs29bpre1  38338  elnn0rabdioph  40541  fiphp3d  40557