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

Theorem elrnmpt1s 5277
Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
Hypotheses
Ref Expression
rnmpt.1 𝐹 = (𝑥𝐴𝐵)
elrnmpt1s.1 (𝑥 = 𝐷𝐵 = 𝐶)
Assertion
Ref Expression
elrnmpt1s ((𝐷𝐴𝐶𝑉) → 𝐶 ∈ ran 𝐹)
Distinct variable groups:   𝑥,𝐶   𝑥,𝐴   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt1s
StepHypRef Expression
1 eqid 2605 . . 3 𝐶 = 𝐶
2 elrnmpt1s.1 . . . . 5 (𝑥 = 𝐷𝐵 = 𝐶)
32eqeq2d 2615 . . . 4 (𝑥 = 𝐷 → (𝐶 = 𝐵𝐶 = 𝐶))
43rspcev 3277 . . 3 ((𝐷𝐴𝐶 = 𝐶) → ∃𝑥𝐴 𝐶 = 𝐵)
51, 4mpan2 702 . 2 (𝐷𝐴 → ∃𝑥𝐴 𝐶 = 𝐵)
6 rnmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐵)
76elrnmpt 5276 . . 3 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
87biimparc 502 . 2 ((∃𝑥𝐴 𝐶 = 𝐵𝐶𝑉) → 𝐶 ∈ ran 𝐹)
95, 8sylan 486 1 ((𝐷𝐴𝐶𝑉) → 𝐶 ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  wrex 2892  cmpt 4633  ran crn 5025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-mpt 4635  df-cnv 5032  df-dm 5034  df-rn 5035
This theorem is referenced by:  wunex2  9412  dfod2  17746  dprd2dlem1  18205  dprd2da  18206  ordtbaslem  20740  subgntr  21658  opnsubg  21659  tgpconcomp  21664  tsmsxplem1  21704  xrge0gsumle  22372  xrge0tsms  22373  minveclem3b  22920  minveclem3  22921  minveclem4  22924  efsubm  24014  dchrisum0fno1  24913  xrge0tsmsd  28918  esumcvg  29277  esum2d  29284  msubco  30484  sge0xaddlem1  39126
  Copyright terms: Public domain W3C validator