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

Theorem ssrexv 3864
Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
Assertion
Ref Expression
ssrexv (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrexv
StepHypRef Expression
1 ssel 3792 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 600 . 2 (𝐴𝐵 → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
32reximdv2 3201 1 (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wrex 3097  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-rex 3102  df-in 3776  df-ss 3783
This theorem is referenced by:  ssn0rex  4137  iunss1  4724  onfr  5975  moriotass  6860  frxp  7517  frfi  8440  fisupcl  8610  supgtoreq  8611  brwdom3  8722  unwdomg  8724  tcrank  8990  hsmexlem2  9530  pwfseqlem3  9763  grur1  9923  suplem1pr  10155  fimaxre2  11250  suprfinzcl  11754  lbzbi  11991  suprzub  11994  uzsupss  11995  zmin  11999  ssnn0fi  13004  elss2prb  13482  scshwfzeqfzo  13792  rexico  14312  rlim3  14448  rlimclim  14496  caurcvgr  14623  alzdvds  15261  bitsfzolem  15371  pclem  15756  0ram2  15938  0ramcl  15940  symgextfo  18039  lsmless1x  18256  lsmless2x  18257  dprdss  18626  ablfac2  18686  subrgdvds  18994  ssrest  21191  locfincf  21545  fbun  21854  fgss  21887  isucn2  22293  metust  22573  psmetutop  22582  lebnumlem3  22972  lebnum  22973  cfil3i  23277  cfilss  23278  fgcfil  23279  iscau4  23287  ivthle  23436  ivthle2  23437  lhop1lem  23989  lhop2  23991  ply1divex  24109  plyss  24168  dgrlem  24198  elqaa  24290  aannenlem2  24297  reeff1olem  24413  rlimcnp  24905  ftalem3  25014  pntlem3  25511  tgisline  25735  axcontlem2  26058  frgrwopreg1  27492  frgrwopreg2  27493  shless  28545  xlt2addrd  29849  ssnnssfz  29875  xreceu  29954  archirngz  30067  archiabllem1b  30070  locfinreflem  30231  crefss  30240  esumpcvgval  30464  sigaclci  30519  eulerpartlemgvv  30762  eulerpartlemgh  30764  signsply0  30952  iccllysconn  31553  frmin  32061  fgmin  32684  knoppndvlem18  32835  poimirlem26  33746  poimirlem30  33750  volsupnfl  33765  cover2  33818  filbcmb  33845  istotbnd3  33879  sstotbnd  33883  heibor1lem  33917  isdrngo2  34066  isdrngo3  34067  qsss1  34368  islsati  34772  paddss1  35595  paddss2  35596  hdmap14lem2a  37645  pellfundre  37944  pellfundge  37945  pellfundglb  37948  hbtlem3  38195  hbtlem5  38196  itgoss  38231  radcnvrat  39010  fiminre2  40071  uzubico  40272  uzubico2  40274  climleltrp  40385  fourierdlem20  40820  smflimlem2  41459  iccelpart  41941  fmtnofac2  42053  ssnn0ssfz  42692  pgrpgt2nabl  42712
  Copyright terms: Public domain W3C validator