Theorem risset 3208

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

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 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-rex 3058

This theorem is referenced by:  nelb  3209  ceqsralv  3478  clel5  3616  reueq  3692  reuind  3708  0el  4312  reusv3  5347  elidinxp  6000  sucel  6390  fvmptt  6958  releldm2  7984  qsid  8714  ttrcltr  9617  zorng  10406  rereccl  11850  nndiv  12182  incexc2  15752  ruclem12  16157  chnfi  18548  conjnmzb  19173  pgpfac1lem2  19997  pgpfac1lem4  20000  mat1dimelbas  22406  mat1dimbas  22407  chmaidscmat  22783  unisngl  23462  fmid  23895  dcubic  26803  addsrid  27927  addsprop  27939  negsprop  27997  mulsrid  28072  mulsprop  28089  onsfi  28303  fusgrn0degnn0  29499  chscllem2  31639  disjunsn  32595  grplsm0l  33412  ballotlemsima  34601  dfon2lem8  35904  brimg  36051  dfrecs2  36066  altopelaltxp  36092  prtlem9  39036  prter2  39053  2llnmat  39696  2lnat  39956  cdlemefrs29bpre1  40569  elnn0rabdioph  42960  fiphp3d  42976  minregex  43691