Theorem ssrexv 3700

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

Syntax hints:   → wi 4   ∈ wcel 2030  ∃wrex 2942   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rex 2947  df-in 3614  df-ss 3621

This theorem is referenced by:  ssn0rex  3969  iunss1  4564  onfr  5801  moriotass  6680  frxp  7332  frfi  8246  fisupcl  8416  supgtoreq  8417  brwdom3  8528  unwdomg  8530  tcrank  8785  hsmexlem2  9287  pwfseqlem3  9520  grur1  9680  suplem1pr  9912  fimaxre2  11007  suprfinzcl  11530  lbzbi  11814  suprzub  11817  uzsupss  11818  zmin  11822  ssnn0fi  12824  elss2prb  13307  scshwfzeqfzo  13618  rexico  14137  rlim3  14273  rlimclim  14321  caurcvgr  14448  alzdvds  15089  bitsfzolem  15203  pclem  15590  0ram2  15772  0ramcl  15774  symgextfo  17888  lsmless1x  18105  lsmless2x  18106  dprdss  18474  ablfac2  18534  subrgdvds  18842  ssrest  21028  locfincf  21382  fbun  21691  fgss  21724  isucn2  22130  metust  22410  psmetutop  22419  lebnumlem3  22809  lebnum  22810  cfil3i  23113  cfilss  23114  fgcfil  23115  iscau4  23123  ivthle  23271  ivthle2  23272  lhop1lem  23821  lhop2  23823  ply1divex  23941  plyss  24000  dgrlem  24030  elqaa  24122  aannenlem2  24129  reeff1olem  24245  rlimcnp  24737  ftalem3  24846  pntlem3  25343  tgisline  25567  axcontlem2  25890  frgrwopreg1  27298  frgrwopreg2  27299  shless  28346  xlt2addrd  29651  ssnnssfz  29677  xreceu  29758  archirngz  29871  archiabllem1b  29874  locfinreflem  30035  crefss  30044  esumpcvgval  30268  sigaclci  30323  eulerpartlemgvv  30566  eulerpartlemgh  30568  signsply0  30756  iccllysconn  31358  frmin  31867  fgmin  32490  knoppndvlem18  32645  poimirlem26  33565  poimirlem30  33569  volsupnfl  33584  cover2  33638  filbcmb  33665  istotbnd3  33700  sstotbnd  33704  heibor1lem  33738  isdrngo2  33887  isdrngo3  33888  qsss1  34194  islsati  34599  paddss1  35421  paddss2  35422  hdmap14lem2a  37476  pellfundre  37762  pellfundge  37763  pellfundglb  37766  hbtlem3  38014  hbtlem5  38015  itgoss  38050  radcnvrat  38830  fiminre2  39907  uzubico  40113  uzubico2  40115  climleltrp  40226  fourierdlem20  40662  smflimlem2  41301  iccelpart  41694  fmtnofac2  41806  ssnn0ssfz  42452  pgrpgt2nabl  42472