Theorem ssrexv 4036

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3141   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rex 3146  df-in 3945  df-ss 3954

This theorem is referenced by:  ss2rexv  4038  ssn0rex  4317  iunss1  4935  onfr  6232  moriotass  7148  frxp  7822  frfi  8765  fisupcl  8935  supgtoreq  8936  brwdom3  9048  unwdomg  9050  tcrank  9315  hsmexlem2  9851  pwfseqlem3  10084  grur1  10244  suplem1pr  10476  fimaxre2  11588  suprfinzcl  12100  lbzbi  12339  suprzub  12342  uzsupss  12343  zmin  12347  ssnn0fi  13356  elss2prb  13848  scshwfzeqfzo  14190  rexico  14715  rlim3  14857  rlimclim  14905  caurcvgr  15032  alzdvds  15672  bitsfzolem  15785  pclem  16177  0ram2  16359  0ramcl  16361  symgextfo  18552  lsmless1x  18771  lsmless2x  18772  dprdss  19153  ablfac2  19213  subrgdvds  19551  ssrest  21786  locfincf  22141  fbun  22450  fgss  22483  isucn2  22890  metust  23170  psmetutop  23179  lebnumlem3  23569  lebnum  23570  cfil3i  23874  cfilss  23875  fgcfil  23876  iscau4  23884  ivthle  24059  ivthle2  24060  lhop1lem  24612  lhop2  24614  ply1divex  24732  plyss  24791  dgrlem  24821  elqaa  24913  aannenlem2  24920  reeff1olem  25036  rlimcnp  25545  ftalem3  25654  2sqreultblem  26026  2sqreunnlem1  26027  2sqreunnltblem  26029  pntlem3  26187  tgisline  26415  axcontlem2  26753  frgrwopreg1  28099  frgrwopreg2  28100  shless  29138  xlt2addrd  30484  ssnnssfz  30512  xreceu  30600  archirngz  30820  archiabllem1b  30823  locfinreflem  31106  crefss  31115  esumpcvgval  31339  sigaclci  31393  eulerpartlemgvv  31636  eulerpartlemgh  31638  signsply0  31823  iccllysconn  32499  satfvsucsuc  32614  frmin  33086  fgmin  33720  knoppndvlem18  33870  poimirlem26  34920  poimirlem30  34924  volsupnfl  34939  cover2  34991  filbcmb  35017  istotbnd3  35051  sstotbnd  35055  heibor1lem  35089  isdrngo2  35238  isdrngo3  35239  qsss1  35547  islsati  36132  paddss1  36955  paddss2  36956  hdmap14lem2a  39005  prjspreln0  39266  pellfundre  39485  pellfundge  39486  pellfundglb  39489  hbtlem3  39734  hbtlem5  39735  itgoss  39770  radcnvrat  40653  fiminre2  41653  uzubico  41851  uzubico2  41853  climleltrp  41964  fourierdlem20  42419  smflimlem2  43055  iccelpart  43600  fmtnofac2  43738  ssnn0ssfz  44404  pgrpgt2nabl  44421  eenglngeehlnmlem1  44731