Theorem ssrexv 3961

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

Syntax hints:   → wi 4   ∈ wcel 2083  ∃wrex 3108   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-rex 3113  df-in 3872  df-ss 3880

This theorem is referenced by:  ss2rexv  3963  ssn0rex  4241  iunss1  4844  onfr  6112  moriotass  7013  frxp  7680  frfi  8616  fisupcl  8786  supgtoreq  8787  brwdom3  8899  unwdomg  8901  tcrank  9166  hsmexlem2  9702  pwfseqlem3  9935  grur1  10095  suplem1pr  10327  fimaxre2  11440  suprfinzcl  11951  lbzbi  12189  suprzub  12192  uzsupss  12193  zmin  12197  ssnn0fi  13207  elss2prb  13695  scshwfzeqfzo  14028  rexico  14551  rlim3  14693  rlimclim  14741  caurcvgr  14868  alzdvds  15507  bitsfzolem  15620  pclem  16008  0ram2  16190  0ramcl  16192  symgextfo  18285  lsmless1x  18503  lsmless2x  18504  dprdss  18872  ablfac2  18932  subrgdvds  19243  ssrest  21472  locfincf  21827  fbun  22136  fgss  22169  isucn2  22575  metust  22855  psmetutop  22864  lebnumlem3  23254  lebnum  23255  cfil3i  23559  cfilss  23560  fgcfil  23561  iscau4  23569  ivthle  23744  ivthle2  23745  lhop1lem  24297  lhop2  24299  ply1divex  24417  plyss  24476  dgrlem  24506  elqaa  24598  aannenlem2  24605  reeff1olem  24721  rlimcnp  25229  ftalem3  25338  2sqreultblem  25710  2sqreunnlem1  25711  2sqreunnltblem  25713  pntlem3  25871  tgisline  26099  axcontlem2  26438  frgrwopreg1  27785  frgrwopreg2  27786  shless  28823  xlt2addrd  30166  ssnnssfz  30194  xreceu  30278  archirngz  30452  archiabllem1b  30455  locfinreflem  30717  crefss  30726  esumpcvgval  30950  sigaclci  31004  eulerpartlemgvv  31247  eulerpartlemgh  31249  signsply0  31434  iccllysconn  32107  satfvsucsuc  32222  frmin  32695  fgmin  33329  knoppndvlem18  33479  poimirlem26  34470  poimirlem30  34474  volsupnfl  34489  cover2  34542  filbcmb  34568  istotbnd3  34602  sstotbnd  34606  heibor1lem  34640  isdrngo2  34789  isdrngo3  34790  qsss1  35098  islsati  35682  paddss1  36505  paddss2  36506  hdmap14lem2a  38555  prjspreln0  38777  pellfundre  38984  pellfundge  38985  pellfundglb  38988  hbtlem3  39233  hbtlem5  39234  itgoss  39269  radcnvrat  40205  fiminre2  41208  uzubico  41407  uzubico2  41409  climleltrp  41520  fourierdlem20  41976  smflimlem2  42612  iccelpart  43097  fmtnofac2  43235  ssnn0ssfz  43897  pgrpgt2nabl  43916  eenglngeehlnmlem1  44227