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

Theorem ssrexv 4011
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 3937 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 611 . 2 (𝐴𝐵 → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
32reximdv2 3161 1 (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wrex 3073  wss 3910
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3074  df-v 3447  df-in 3917  df-ss 3927
This theorem is referenced by:  ss2rexv  4013  ssn0rex  4315  iunss1  4968  onfr  6356  moriotass  7346  frxp  8058  frfi  9232  fisupcl  9405  supgtoreq  9406  brwdom3  9518  unwdomg  9520  frmin  9685  tcrank  9820  hsmexlem2  10363  pwfseqlem3  10596  grur1  10756  suplem1pr  10988  fimaxre2  12100  fiminre2  12103  suprfinzcl  12617  lbzbi  12861  suprzub  12864  uzsupss  12865  zmin  12869  ssnn0fi  13890  elss2prb  14386  scshwfzeqfzo  14715  rexico  15238  rlim3  15380  rlimclim  15428  caurcvgr  15558  alzdvds  16202  bitsfzolem  16314  pclem  16710  0ram2  16893  0ramcl  16895  symgextfo  19204  lsmless1x  19426  lsmless2x  19427  dprdss  19808  ablfac2  19868  subrgdvds  20236  ssrest  22527  locfincf  22882  fbun  23191  fgss  23224  isucn2  23631  metust  23914  psmetutop  23923  lebnumlem3  24326  lebnum  24327  cfil3i  24633  cfilss  24634  fgcfil  24635  iscau4  24643  ivthle  24820  ivthle2  24821  lhop1lem  25377  lhop2  25379  ply1divex  25501  plyss  25560  dgrlem  25590  elqaa  25682  aannenlem2  25689  reeff1olem  25805  rlimcnp  26315  ftalem3  26424  2sqreultblem  26796  2sqreunnlem1  26797  2sqreunnltblem  26799  pntlem3  26957  madess  27206  addsunif  27310  tgisline  27569  axcontlem2  27914  frgrwopreg1  29262  frgrwopreg2  29263  shless  30301  xlt2addrd  31663  ssnnssfz  31690  xreceu  31778  archirngz  32025  archiabllem1b  32028  locfinreflem  32421  crefss  32430  esumpcvgval  32677  sigaclci  32731  eulerpartlemgvv  32976  eulerpartlemgh  32978  signsply0  33163  iccllysconn  33844  satfvsucsuc  33959  fgmin  34842  knoppndvlem18  34992  poimirlem26  36104  poimirlem30  36108  volsupnfl  36123  cover2  36173  filbcmb  36199  istotbnd3  36230  sstotbnd  36234  heibor1lem  36268  isdrngo2  36417  isdrngo3  36418  qsss1  36749  islsati  37456  paddss1  38280  paddss2  38281  hdmap14lem2a  40330  prjspreln0  40933  pellfundre  41190  pellfundge  41191  pellfundglb  41194  hbtlem3  41440  hbtlem5  41441  itgoss  41476  radcnvrat  42584  uzubico  43796  uzubico2  43798  climleltrp  43907  fourierdlem20  44358  smflimlem2  45003  iccelpart  45615  fmtnofac2  45751  ssnn0ssfz  46415  pgrpgt2nabl  46432  eenglngeehlnmlem1  46813
  Copyright terms: Public domain W3C validator