Theorem ssrexv 3968

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3062   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  ss2rexv  3970  ssn0rex  4270  iunss1  4918  onfr  6252  moriotass  7203  frxp  7893  frfi  8916  fisupcl  9085  supgtoreq  9086  brwdom3  9198  unwdomg  9200  frmin  9365  tcrank  9500  hsmexlem2  10041  pwfseqlem3  10274  grur1  10434  suplem1pr  10666  fimaxre2  11777  fiminre2  11780  suprfinzcl  12292  lbzbi  12532  suprzub  12535  uzsupss  12536  zmin  12540  ssnn0fi  13558  elss2prb  14053  scshwfzeqfzo  14391  rexico  14917  rlim3  15059  rlimclim  15107  caurcvgr  15237  alzdvds  15881  bitsfzolem  15993  pclem  16391  0ram2  16574  0ramcl  16576  symgextfo  18814  lsmless1x  19033  lsmless2x  19034  dprdss  19416  ablfac2  19476  subrgdvds  19814  ssrest  22073  locfincf  22428  fbun  22737  fgss  22770  isucn2  23176  metust  23456  psmetutop  23465  lebnumlem3  23860  lebnum  23861  cfil3i  24166  cfilss  24167  fgcfil  24168  iscau4  24176  ivthle  24353  ivthle2  24354  lhop1lem  24910  lhop2  24912  ply1divex  25034  plyss  25093  dgrlem  25123  elqaa  25215  aannenlem2  25222  reeff1olem  25338  rlimcnp  25848  ftalem3  25957  2sqreultblem  26329  2sqreunnlem1  26330  2sqreunnltblem  26332  pntlem3  26490  tgisline  26718  axcontlem2  27056  frgrwopreg1  28401  frgrwopreg2  28402  shless  29440  xlt2addrd  30801  ssnnssfz  30828  xreceu  30916  archirngz  31162  archiabllem1b  31165  locfinreflem  31504  crefss  31513  esumpcvgval  31758  sigaclci  31812  eulerpartlemgvv  32055  eulerpartlemgh  32057  signsply0  32242  iccllysconn  32925  satfvsucsuc  33040  madess  33796  fgmin  34296  knoppndvlem18  34446  poimirlem26  35540  poimirlem30  35544  volsupnfl  35559  cover2  35609  filbcmb  35635  istotbnd3  35666  sstotbnd  35670  heibor1lem  35704  isdrngo2  35853  isdrngo3  35854  qsss1  36160  islsati  36745  paddss1  37568  paddss2  37569  hdmap14lem2a  39618  prjspreln0  40156  pellfundre  40406  pellfundge  40407  pellfundglb  40410  hbtlem3  40655  hbtlem5  40656  itgoss  40691  radcnvrat  41605  uzubico  42781  uzubico2  42783  climleltrp  42892  fourierdlem20  43343  smflimlem2  43979  iccelpart  44558  fmtnofac2  44694  ssnn0ssfz  45358  pgrpgt2nabl  45375  eenglngeehlnmlem1  45756