Theorem ssrexv 3984

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

Step	Hyp	Ref	Expression
1		ssel 3910	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 610	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	reximdv2 3198	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3064   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ss2rexv  3986  ssn0rex  4286  iunss1  4935  onfr  6290  moriotass  7245  frxp  7938  frfi  8989  fisupcl  9158  supgtoreq  9159  brwdom3  9271  unwdomg  9273  frmin  9438  tcrank  9573  hsmexlem2  10114  pwfseqlem3  10347  grur1  10507  suplem1pr  10739  fimaxre2  11850  fiminre2  11853  suprfinzcl  12365  lbzbi  12605  suprzub  12608  uzsupss  12609  zmin  12613  ssnn0fi  13633  elss2prb  14129  scshwfzeqfzo  14467  rexico  14993  rlim3  15135  rlimclim  15183  caurcvgr  15313  alzdvds  15957  bitsfzolem  16069  pclem  16467  0ram2  16650  0ramcl  16652  symgextfo  18945  lsmless1x  19164  lsmless2x  19165  dprdss  19547  ablfac2  19607  subrgdvds  19953  ssrest  22235  locfincf  22590  fbun  22899  fgss  22932  isucn2  23339  metust  23620  psmetutop  23629  lebnumlem3  24032  lebnum  24033  cfil3i  24338  cfilss  24339  fgcfil  24340  iscau4  24348  ivthle  24525  ivthle2  24526  lhop1lem  25082  lhop2  25084  ply1divex  25206  plyss  25265  dgrlem  25295  elqaa  25387  aannenlem2  25394  reeff1olem  25510  rlimcnp  26020  ftalem3  26129  2sqreultblem  26501  2sqreunnlem1  26502  2sqreunnltblem  26504  pntlem3  26662  tgisline  26892  axcontlem2  27236  frgrwopreg1  28583  frgrwopreg2  28584  shless  29622  xlt2addrd  30983  ssnnssfz  31010  xreceu  31098  archirngz  31345  archiabllem1b  31348  locfinreflem  31692  crefss  31701  esumpcvgval  31946  sigaclci  32000  eulerpartlemgvv  32243  eulerpartlemgh  32245  signsply0  32430  iccllysconn  33112  satfvsucsuc  33227  madess  33986  fgmin  34486  knoppndvlem18  34636  poimirlem26  35730  poimirlem30  35734  volsupnfl  35749  cover2  35799  filbcmb  35825  istotbnd3  35856  sstotbnd  35860  heibor1lem  35894  isdrngo2  36043  isdrngo3  36044  qsss1  36350  islsati  36935  paddss1  37758  paddss2  37759  hdmap14lem2a  39808  prjspreln0  40369  pellfundre  40619  pellfundge  40620  pellfundglb  40623  hbtlem3  40868  hbtlem5  40869  itgoss  40904  radcnvrat  41821  uzubico  42996  uzubico2  42998  climleltrp  43107  fourierdlem20  43558  smflimlem2  44194  iccelpart  44773  fmtnofac2  44909  ssnn0ssfz  45573  pgrpgt2nabl  45590  eenglngeehlnmlem1  45971