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

Theorem ssrexv 4016
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 3942 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 612 . 2 (𝐴𝐵 → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
32reximdv2 3162 1 (𝐴𝐵 → (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wrex 3074  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  ss2rexv  4018  ssn0rex  4320  iunss1  4973  onfr  6361  moriotass  7351  frxp  8063  frfi  9239  fisupcl  9412  supgtoreq  9413  brwdom3  9525  unwdomg  9527  frmin  9692  tcrank  9827  hsmexlem2  10370  pwfseqlem3  10603  grur1  10763  suplem1pr  10995  fimaxre2  12107  fiminre2  12110  suprfinzcl  12624  lbzbi  12868  suprzub  12871  uzsupss  12872  zmin  12876  ssnn0fi  13897  elss2prb  14393  scshwfzeqfzo  14722  rexico  15245  rlim3  15387  rlimclim  15435  caurcvgr  15565  alzdvds  16209  bitsfzolem  16321  pclem  16717  0ram2  16900  0ramcl  16902  symgextfo  19211  lsmless1x  19433  lsmless2x  19434  dprdss  19815  ablfac2  19875  subrgdvds  20252  ssrest  22543  locfincf  22898  fbun  23207  fgss  23240  isucn2  23647  metust  23930  psmetutop  23939  lebnumlem3  24342  lebnum  24343  cfil3i  24649  cfilss  24650  fgcfil  24651  iscau4  24659  ivthle  24836  ivthle2  24837  lhop1lem  25393  lhop2  25395  ply1divex  25517  plyss  25576  dgrlem  25606  elqaa  25698  aannenlem2  25705  reeff1olem  25821  rlimcnp  26331  ftalem3  26440  2sqreultblem  26812  2sqreunnlem1  26813  2sqreunnltblem  26815  pntlem3  26973  madess  27228  addsunif  27332  tgisline  27611  axcontlem2  27956  frgrwopreg1  29304  frgrwopreg2  29305  shless  30343  xlt2addrd  31705  ssnnssfz  31732  xreceu  31820  archirngz  32067  archiabllem1b  32070  locfinreflem  32461  crefss  32470  esumpcvgval  32717  sigaclci  32771  eulerpartlemgvv  33016  eulerpartlemgh  33018  signsply0  33203  iccllysconn  33884  satfvsucsuc  33999  fgmin  34871  knoppndvlem18  35021  poimirlem26  36133  poimirlem30  36137  volsupnfl  36152  cover2  36202  filbcmb  36228  istotbnd3  36259  sstotbnd  36263  heibor1lem  36297  isdrngo2  36446  isdrngo3  36447  qsss1  36778  islsati  37485  paddss1  38309  paddss2  38310  hdmap14lem2a  40359  prjspreln0  40976  pellfundre  41233  pellfundge  41234  pellfundglb  41237  hbtlem3  41483  hbtlem5  41484  itgoss  41519  radcnvrat  42668  uzubico  43880  uzubico2  43882  climleltrp  43991  fourierdlem20  44442  smflimlem2  45087  iccelpart  45699  fmtnofac2  45835  ssnn0ssfz  46499  pgrpgt2nabl  46516  eenglngeehlnmlem1  46897
  Copyright terms: Public domain W3C validator