Theorem ssrexv 3800

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

Syntax hints:   → wi 4   ∈ wcel 2131  ∃wrex 3043   ⊆ wss 3707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-rex 3048  df-in 3714  df-ss 3721

This theorem is referenced by:  ssn0rex  4071  iunss1  4676  onfr  5916  moriotass  6795  frxp  7447  frfi  8362  fisupcl  8532  supgtoreq  8533  brwdom3  8644  unwdomg  8646  tcrank  8912  hsmexlem2  9433  pwfseqlem3  9666  grur1  9826  suplem1pr  10058  fimaxre2  11153  suprfinzcl  11676  lbzbi  11961  suprzub  11964  uzsupss  11965  zmin  11969  ssnn0fi  12970  elss2prb  13453  scshwfzeqfzo  13764  rexico  14284  rlim3  14420  rlimclim  14468  caurcvgr  14595  alzdvds  15236  bitsfzolem  15350  pclem  15737  0ram2  15919  0ramcl  15921  symgextfo  18034  lsmless1x  18251  lsmless2x  18252  dprdss  18620  ablfac2  18680  subrgdvds  18988  ssrest  21174  locfincf  21528  fbun  21837  fgss  21870  isucn2  22276  metust  22556  psmetutop  22565  lebnumlem3  22955  lebnum  22956  cfil3i  23259  cfilss  23260  fgcfil  23261  iscau4  23269  ivthle  23417  ivthle2  23418  lhop1lem  23967  lhop2  23969  ply1divex  24087  plyss  24146  dgrlem  24176  elqaa  24268  aannenlem2  24275  reeff1olem  24391  rlimcnp  24883  ftalem3  24992  pntlem3  25489  tgisline  25713  axcontlem2  26036  frgrwopreg1  27464  frgrwopreg2  27465  shless  28519  xlt2addrd  29824  ssnnssfz  29850  xreceu  29931  archirngz  30044  archiabllem1b  30047  locfinreflem  30208  crefss  30217  esumpcvgval  30441  sigaclci  30496  eulerpartlemgvv  30739  eulerpartlemgh  30741  signsply0  30929  iccllysconn  31531  frmin  32040  fgmin  32663  knoppndvlem18  32818  poimirlem26  33740  poimirlem30  33744  volsupnfl  33759  cover2  33813  filbcmb  33840  istotbnd3  33875  sstotbnd  33879  heibor1lem  33913  isdrngo2  34062  isdrngo3  34063  qsss1  34369  islsati  34776  paddss1  35598  paddss2  35599  hdmap14lem2a  37653  pellfundre  37939  pellfundge  37940  pellfundglb  37943  hbtlem3  38191  hbtlem5  38192  itgoss  38227  radcnvrat  39007  fiminre2  40084  uzubico  40290  uzubico2  40292  climleltrp  40403  fourierdlem20  40839  smflimlem2  41478  iccelpart  41871  fmtnofac2  41983  ssnn0ssfz  42629  pgrpgt2nabl  42649