Theorem ssrexv 4016

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3069   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ss2rexv  4018  ssn0rex  4320  iunss1  4973  onfr  6361  moriotass  7351  frxp  8063  frfi  9239  fisupcl  9414  supgtoreq  9415  brwdom3  9527  unwdomg  9529  frmin  9694  tcrank  9829  hsmexlem2  10372  pwfseqlem3  10605  grur1  10765  suplem1pr  10997  fimaxre2  12109  fiminre2  12112  suprfinzcl  12626  lbzbi  12870  suprzub  12873  uzsupss  12874  zmin  12878  ssnn0fi  13900  elss2prb  14398  scshwfzeqfzo  14727  rexico  15250  rlim3  15392  rlimclim  15440  caurcvgr  15570  alzdvds  16213  bitsfzolem  16325  pclem  16721  0ram2  16904  0ramcl  16906  symgextfo  19218  lsmless1x  19440  lsmless2x  19441  dprdss  19822  ablfac2  19882  subrgdvds  20284  ssrest  22564  locfincf  22919  fbun  23228  fgss  23261  isucn2  23668  metust  23951  psmetutop  23960  lebnumlem3  24363  lebnum  24364  cfil3i  24670  cfilss  24671  fgcfil  24672  iscau4  24680  ivthle  24857  ivthle2  24858  lhop1lem  25414  lhop2  25416  ply1divex  25538  plyss  25597  dgrlem  25627  elqaa  25719  aannenlem2  25726  reeff1olem  25842  rlimcnp  26352  ftalem3  26461  2sqreultblem  26833  2sqreunnlem1  26834  2sqreunnltblem  26836  pntlem3  26994  madess  27249  addsunif  27353  tgisline  27632  axcontlem2  27977  frgrwopreg1  29325  frgrwopreg2  29326  shless  30364  xlt2addrd  31731  ssnnssfz  31758  xreceu  31848  archirngz  32095  archiabllem1b  32098  locfinreflem  32510  crefss  32519  esumpcvgval  32766  sigaclci  32820  eulerpartlemgvv  33065  eulerpartlemgh  33067  signsply0  33252  iccllysconn  33931  satfvsucsuc  34046  fgmin  34918  knoppndvlem18  35068  poimirlem26  36177  poimirlem30  36181  volsupnfl  36196  cover2  36246  filbcmb  36272  istotbnd3  36303  sstotbnd  36307  heibor1lem  36341  isdrngo2  36490  isdrngo3  36491  qsss1  36822  islsati  37529  paddss1  38353  paddss2  38354  hdmap14lem2a  40403  prjspreln0  41005  pellfundre  41262  pellfundge  41263  pellfundglb  41266  hbtlem3  41512  hbtlem5  41513  itgoss  41548  radcnvrat  42716  uzubico  43926  uzubico2  43928  climleltrp  44037  fourierdlem20  44488  smflimlem2  45133  iccelpart  45745  fmtnofac2  45881  ssnn0ssfz  46545  pgrpgt2nabl  46562  eenglngeehlnmlem1  46943