Theorem ssrexv 3629

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

Syntax hints:   → wi 4   ∈ wcel 1976  ∃wrex 2896   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-rex 2901  df-in 3546  df-ss 3553

This theorem is referenced by:  iunss1  4462  onfr  5666  moriotass  6517  frxp  7152  frfi  8068  fisupcl  8236  supgtoreq  8237  brwdom3  8348  unwdomg  8350  tcrank  8608  hsmexlem2  9110  pwfseqlem3  9339  grur1  9499  suplem1pr  9731  fimaxre2  10821  suprfinzcl  11327  lbzbi  11611  suprzub  11614  uzsupss  11615  zmin  11619  ssnn0fi  12604  elss2prb  13076  scshwfzeqfzo  13372  rexico  13890  rlim3  14026  rlimclim  14074  caurcvgr  14201  alzdvds  14829  bitsfzolem  14943  pclem  15330  0ram2  15512  0ramcl  15514  symgextfo  17614  lsmless1x  17831  lsmless2x  17832  dprdss  18200  ablfac2  18260  subrgdvds  18566  ssrest  20738  locfincf  21092  fbun  21402  fgss  21435  isucn2  21841  metust  22121  psmetutop  22130  lebnumlem3  22518  lebnum  22519  cfil3i  22820  cfilss  22821  fgcfil  22822  iscau4  22830  ivthle  22977  ivthle2  22978  lhop1lem  23525  lhop2  23527  ply1divex  23645  plyss  23704  dgrlem  23734  elqaa  23826  aannenlem2  23833  reeff1olem  23949  rlimcnp  24437  ftalem3  24546  pntlem3  25043  tgisline  25268  axcontlem2  25591  frgrawopreg1  26371  frgrawopreg2  26372  shless  27436  xlt2addrd  28747  ssnnssfz  28771  xreceu  28795  archirngz  28908  archiabllem1b  28911  locfinreflem  29069  crefss  29078  esumpcvgval  29301  sigaclci  29356  eulerpartlemgvv  29599  eulerpartlemgh  29601  signsply0  29788  iccllyscon  30320  frmin  30817  nodenselem4  30917  fgmin  31369  knoppndvlem18  31524  poimirlem26  32429  poimirlem30  32433  volsupnfl  32448  cover2  32502  filbcmb  32529  istotbnd3  32564  sstotbnd  32568  heibor1lem  32602  isdrngo2  32751  isdrngo3  32752  islsati  33123  paddss1  33945  paddss2  33946  hdmap14lem2a  36001  pellfundre  36287  pellfundge  36288  pellfundglb  36291  hbtlem3  36540  hbtlem5  36541  itgoss  36576  radcnvrat  37359  fiminre2  38359  climleltrp  38567  fourierdlem20  38844  smflimlem2  39482  iccelpart  39796  fmtnofac2  39844  ssn0rex  40136  frgrwopreg1  41509  frgrwopreg2  41510  ssnn0ssfz  41942  pgrpgt2nabl  41963