Theorem ssrexv 3989

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 3915	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	reximdv2 3200	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3066   ⊆ wss 3888

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rex 3071  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  ss2rexv  3991  ssn0rex  4290  iunss1  4939  onfr  6309  moriotass  7274  frxp  7976  frfi  9068  fisupcl  9237  supgtoreq  9238  brwdom3  9350  unwdomg  9352  frmin  9516  tcrank  9651  hsmexlem2  10192  pwfseqlem3  10425  grur1  10585  suplem1pr  10817  fimaxre2  11929  fiminre2  11932  suprfinzcl  12445  lbzbi  12685  suprzub  12688  uzsupss  12689  zmin  12693  ssnn0fi  13714  elss2prb  14210  scshwfzeqfzo  14548  rexico  15074  rlim3  15216  rlimclim  15264  caurcvgr  15394  alzdvds  16038  bitsfzolem  16150  pclem  16548  0ram2  16731  0ramcl  16733  symgextfo  19039  lsmless1x  19258  lsmless2x  19259  dprdss  19641  ablfac2  19701  subrgdvds  20047  ssrest  22336  locfincf  22691  fbun  23000  fgss  23033  isucn2  23440  metust  23723  psmetutop  23732  lebnumlem3  24135  lebnum  24136  cfil3i  24442  cfilss  24443  fgcfil  24444  iscau4  24452  ivthle  24629  ivthle2  24630  lhop1lem  25186  lhop2  25188  ply1divex  25310  plyss  25369  dgrlem  25399  elqaa  25491  aannenlem2  25498  reeff1olem  25614  rlimcnp  26124  ftalem3  26233  2sqreultblem  26605  2sqreunnlem1  26606  2sqreunnltblem  26608  pntlem3  26766  tgisline  26997  axcontlem2  27342  frgrwopreg1  28691  frgrwopreg2  28692  shless  29730  xlt2addrd  31090  ssnnssfz  31117  xreceu  31205  archirngz  31452  archiabllem1b  31455  locfinreflem  31799  crefss  31808  esumpcvgval  32055  sigaclci  32109  eulerpartlemgvv  32352  eulerpartlemgh  32354  signsply0  32539  iccllysconn  33221  satfvsucsuc  33336  madess  34068  fgmin  34568  knoppndvlem18  34718  poimirlem26  35812  poimirlem30  35816  volsupnfl  35831  cover2  35881  filbcmb  35907  istotbnd3  35938  sstotbnd  35942  heibor1lem  35976  isdrngo2  36125  isdrngo3  36126  qsss1  36431  islsati  37015  paddss1  37838  paddss2  37839  hdmap14lem2a  39888  prjspreln0  40455  pellfundre  40710  pellfundge  40711  pellfundglb  40714  hbtlem3  40959  hbtlem5  40960  itgoss  40995  radcnvrat  41939  uzubico  43113  uzubico2  43115  climleltrp  43224  fourierdlem20  43675  smflimlem2  44317  iccelpart  44896  fmtnofac2  45032  ssnn0ssfz  45696  pgrpgt2nabl  45713  eenglngeehlnmlem1  46094