Theorem risset 3242

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 1894	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3092	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2841	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 307	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-rex 3092

This theorem is used by:  nelb  3243  ceqsralv  3497  clel5  3626  reueq  3702  reuind  3718  0el  4318  reusv3  5378  elidinxp  6048  sucel  6441  fvmptt  7014  releldm2  8042  qsid  8781  ttrcltr  9688  zorng  10499  rereccl  11944  nndiv  12293  incexc2  15910  ruclem12  16314  chnfi  18707  conjnmzb  19346  pgpfac1lem2  20170  pgpfac1lem4  20173  mat1dimelbas  22657  mat1dimbas  22658  chmaidscmat  23034  unisngl  23713  fmid  24146  dcubic  27040  addsrid  28186  addsprop  28198  negsprop  28257  mulsrid  28335  mulsprop  28352  onsfi  28578  fusgrn0degnn0  29878  chscllem2  32019  disjunsn  32968  grplsm0l  33735  ballotlemsima  34930  dfon2lem8  36293  brimg  36440  dfrecs2  36455  altopelaltxp  36481  prtlem9  39671  prter2  39688  2llnmat  40331  2lnat  40591  cdlemefrs29bpre1  41204  elnn0rabdioph  43563  fiphp3d  43579  minregex  44293