Theorem ssrexv 4037

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3142   ⊆ wss 3939

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 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-rex 3147  df-in 3946  df-ss 3955

This theorem is referenced by:  ss2rexv  4039  ssn0rex  4318  iunss1  4936  onfr  6233  moriotass  7149  frxp  7823  frfi  8766  fisupcl  8936  supgtoreq  8937  brwdom3  9049  unwdomg  9051  tcrank  9316  hsmexlem2  9852  pwfseqlem3  10085  grur1  10245  suplem1pr  10477  fimaxre2  11589  suprfinzcl  12100  lbzbi  12339  suprzub  12342  uzsupss  12343  zmin  12347  ssnn0fi  13356  elss2prb  13848  scshwfzeqfzo  14191  rexico  14716  rlim3  14858  rlimclim  14906  caurcvgr  15033  alzdvds  15673  bitsfzolem  15786  pclem  16178  0ram2  16360  0ramcl  16362  symgextfo  18553  lsmless1x  18772  lsmless2x  18773  dprdss  19154  ablfac2  19214  subrgdvds  19552  ssrest  21787  locfincf  22142  fbun  22451  fgss  22484  isucn2  22891  metust  23171  psmetutop  23180  lebnumlem3  23570  lebnum  23571  cfil3i  23875  cfilss  23876  fgcfil  23877  iscau4  23885  ivthle  24060  ivthle2  24061  lhop1lem  24613  lhop2  24615  ply1divex  24733  plyss  24792  dgrlem  24822  elqaa  24914  aannenlem2  24921  reeff1olem  25037  rlimcnp  25546  ftalem3  25655  2sqreultblem  26027  2sqreunnlem1  26028  2sqreunnltblem  26030  pntlem3  26188  tgisline  26416  axcontlem2  26754  frgrwopreg1  28100  frgrwopreg2  28101  shless  29139  xlt2addrd  30485  ssnnssfz  30513  xreceu  30602  archirngz  30822  archiabllem1b  30825  locfinreflem  31108  crefss  31117  esumpcvgval  31341  sigaclci  31395  eulerpartlemgvv  31638  eulerpartlemgh  31640  signsply0  31825  iccllysconn  32501  satfvsucsuc  32616  frmin  33088  fgmin  33722  knoppndvlem18  33872  poimirlem26  34922  poimirlem30  34926  volsupnfl  34941  cover2  34993  filbcmb  35019  istotbnd3  35053  sstotbnd  35057  heibor1lem  35091  isdrngo2  35240  isdrngo3  35241  qsss1  35549  islsati  36134  paddss1  36957  paddss2  36958  hdmap14lem2a  39007  prjspreln0  39265  pellfundre  39484  pellfundge  39485  pellfundglb  39488  hbtlem3  39733  hbtlem5  39734  itgoss  39769  radcnvrat  40652  fiminre2  41652  uzubico  41850  uzubico2  41852  climleltrp  41963  fourierdlem20  42419  smflimlem2  43055  iccelpart  43600  fmtnofac2  43738  ssnn0ssfz  44404  pgrpgt2nabl  44421  eenglngeehlnmlem1  44731