Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elima Structured version   Visualization version   GIF version

Theorem elima 5902
 Description: Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
Hypothesis
Ref Expression
elima.1 𝐴 ∈ V
Assertion
Ref Expression
elima (𝐴 ∈ (𝐵𝐶) ↔ ∃𝑥𝐶 𝑥𝐵𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem elima
StepHypRef Expression
1 elima.1 . 2 𝐴 ∈ V
2 elimag 5901 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ ∃𝑥𝐶 𝑥𝐵𝐴))
31, 2ax-mp 5 1 (𝐴 ∈ (𝐵𝐶) ↔ ∃𝑥𝐶 𝑥𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441   class class class wbr 5031   “ cima 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032  df-opab 5094  df-xp 5526  df-cnv 5528  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533 This theorem is referenced by:  elima2  5903  rninxp  6004  imaco  6072  isarep1  6413  eliman0  6681  funimass4  6706  isomin  7070  dfsup2  8895  dfac10b  9553  hausmapdom  22115  pi1blem  23654  adjbd1o  29878  imaindm  33150  scutun12  33399  madeval2  33418  brimage  33515  dfrecs2  33539  dfrdg4  33540  dfint3  33541  imagesset  33542  elimaint  40392  elintima  40397
 Copyright terms: Public domain W3C validator