Theorem risset 3221

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

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

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 2810  df-rex 3062

This theorem is referenced by:  nelb  3222  ceqsralv  3506  clel5  3649  reueq  3725  reuind  3741  0el  4343  iunidOLD  5042  reusv3  5380  elidinxp  6036  sucel  6433  fvmptt  7011  releldm2  8047  qsid  8802  ttrcltr  9735  zorng  10523  rereccl  11964  nndiv  12291  incexc2  15859  ruclem12  16264  conjnmzb  19241  pgpfac1lem2  20063  pgpfac1lem4  20066  mat1dimelbas  22414  mat1dimbas  22415  chmaidscmat  22791  unisngl  23470  fmid  23903  dcubic  26813  addsrid  27928  addsprop  27940  negsprop  27998  mulsrid  28073  mulsprop  28090  onsfi  28304  fusgrn0degnn0  29484  chscllem2  31624  disjunsn  32580  grplsm0l  33423  ballotlemsima  34553  dfon2lem8  35813  brimg  35960  dfrecs2  35973  altopelaltxp  35999  prtlem9  38887  prter2  38904  2llnmat  39548  2lnat  39808  cdlemefrs29bpre1  40421  elnn0rabdioph  42801  fiphp3d  42817  minregex  43533