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

Theorem elima 5611
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 5610 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ ∃𝑥𝐶 𝑥𝐵𝐴))
31, 2ax-mp 5 1 (𝐴 ∈ (𝐵𝐶) ↔ ∃𝑥𝐶 𝑥𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 2145  wrex 3062  Vcvv 3351   class class class wbr 4787  cima 5253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-xp 5256  df-cnv 5258  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263
This theorem is referenced by:  elima2  5612  rninxp  5713  imaco  5783  isarep1  6116  eliman0  6366  funimass4  6391  isomin  6733  dfsup2  8510  dfac10b  9167  hausmapdom  21524  pi1blem  23058  adjbd1o  29284  elintfv  32000  imaindm  32018  scutun12  32254  madeval2  32273  brimage  32370  dfrecs2  32394  dfrdg4  32395  dfint3  32396  imagesset  32397  elimaint  38464  elintima  38469
  Copyright terms: Public domain W3C validator