Theorem risset 3177

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1542  ∃wex 1786   ∈ wcel 2114  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-clel 2811  df-rex 3059

This theorem is referenced by:  nelb  3178  ceqsralv  3435  clel5  3563  reueq  3636  reuind  3652  0el  4249  iunid  4946  reusv3  5272  elidinxp  5885  sucel  6245  fvmptt  6795  releldm2  7767  qsid  8394  zorng  10004  rereccl  11436  nndiv  11762  incexc2  15286  ruclem12  15686  conjnmzb  18511  pgpfac1lem2  19316  pgpfac1lem4  19319  mat1dimelbas  21222  mat1dimbas  21223  chmaidscmat  21599  unisngl  22278  fmid  22711  dcubic  25584  fusgrn0degnn0  27441  chscllem2  29573  disjunsn  30507  grplsm0l  31163  ballotlemsima  32052  dfon2lem8  33338  addsid1  33765  brimg  33877  dfrecs2  33890  altopelaltxp  33916  prtlem9  36501  prter2  36518  2llnmat  37161  2lnat  37421  cdlemefrs29bpre1  38034  elnn0rabdioph  40197  fiphp3d  40213