Theorem ssrexv 4050

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3068   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  ss2rexv  4052  ssn0rex  4354  iunss1  5010  onfr  6402  moriotass  7400  frxp  8114  frfi  9290  fisupcl  9466  supgtoreq  9467  brwdom3  9579  unwdomg  9581  frmin  9746  tcrank  9881  hsmexlem2  10424  pwfseqlem3  10657  grur1  10817  suplem1pr  11049  fimaxre2  12163  fiminre2  12166  suprfinzcl  12680  lbzbi  12924  suprzub  12927  uzsupss  12928  zmin  12932  ssnn0fi  13954  elss2prb  14452  scshwfzeqfzo  14781  rexico  15304  rlim3  15446  rlimclim  15494  caurcvgr  15624  alzdvds  16267  bitsfzolem  16379  pclem  16775  0ram2  16958  0ramcl  16960  symgextfo  19331  lsmless1x  19553  lsmless2x  19554  dprdss  19940  ablfac2  20000  subrgdvds  20476  ssrest  22900  locfincf  23255  fbun  23564  fgss  23597  isucn2  24004  metust  24287  psmetutop  24296  lebnumlem3  24709  lebnum  24710  cfil3i  25017  cfilss  25018  fgcfil  25019  iscau4  25027  ivthle  25205  ivthle2  25206  lhop1lem  25765  lhop2  25767  ply1divex  25889  plyss  25948  dgrlem  25978  elqaa  26071  aannenlem2  26078  reeff1olem  26194  rlimcnp  26706  ftalem3  26815  2sqreultblem  27187  2sqreunnlem1  27188  2sqreunnltblem  27190  pntlem3  27348  madess  27608  addsuniflem  27723  mulsuniflem  27843  tgisline  28145  axcontlem2  28490  frgrwopreg1  29838  frgrwopreg2  29839  shless  30879  xlt2addrd  32238  ssnnssfz  32265  xreceu  32355  archirngz  32605  archiabllem1b  32608  locfinreflem  33118  crefss  33127  esumpcvgval  33374  sigaclci  33428  eulerpartlemgvv  33673  eulerpartlemgh  33675  signsply0  33860  iccllysconn  34539  satfvsucsuc  34654  fgmin  35558  knoppndvlem18  35708  poimirlem26  36817  poimirlem30  36821  volsupnfl  36836  cover2  36886  filbcmb  36911  istotbnd3  36942  sstotbnd  36946  heibor1lem  36980  isdrngo2  37129  isdrngo3  37130  qsss1  37460  islsati  38167  paddss1  38991  paddss2  38992  hdmap14lem2a  41041  prjspreln0  41653  pellfundre  41921  pellfundge  41922  pellfundglb  41925  hbtlem3  42171  hbtlem5  42172  itgoss  42207  radcnvrat  43375  uzubico  44579  uzubico2  44581  climleltrp  44690  fourierdlem20  45141  smflimlem2  45786  iccelpart  46399  fmtnofac2  46535  ssnn0ssfz  47113  pgrpgt2nabl  47130  eenglngeehlnmlem1  47510