Theorem risset 3204

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  3205  ceqsralv  3479  clel5  3622  reueq  3699  reuind  3715  0el  4316  iunidOLD  5013  reusv3  5347  elidinxp  5999  sucel  6387  fvmptt  6954  releldm2  7985  qsid  8715  ttrcltr  9631  zorng  10417  rereccl  11860  nndiv  12192  incexc2  15763  ruclem12  16168  conjnmzb  19150  pgpfac1lem2  19974  pgpfac1lem4  19977  mat1dimelbas  22374  mat1dimbas  22375  chmaidscmat  22751  unisngl  23430  fmid  23863  dcubic  26772  addsrid  27894  addsprop  27906  negsprop  27964  mulsrid  28039  mulsprop  28056  onsfi  28270  fusgrn0degnn0  29463  chscllem2  31600  disjunsn  32556  grplsm0l  33353  ballotlemsima  34486  dfon2lem8  35766  brimg  35913  dfrecs2  35926  altopelaltxp  35952  prtlem9  38845  prter2  38862  2llnmat  39506  2lnat  39766  cdlemefrs29bpre1  40379  elnn0rabdioph  42779  fiphp3d  42795  minregex  43510