Theorem ssrexv 3667

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rex 2918  df-in 3581  df-ss 3588

This theorem is referenced by:  ssn0rex  3936  iunss1  4532  onfr  5763  moriotass  6640  frxp  7287  frfi  8205  fisupcl  8375  supgtoreq  8376  brwdom3  8487  unwdomg  8489  tcrank  8747  hsmexlem2  9249  pwfseqlem3  9482  grur1  9642  suplem1pr  9874  fimaxre2  10969  suprfinzcl  11492  lbzbi  11776  suprzub  11779  uzsupss  11780  zmin  11784  ssnn0fi  12784  elss2prb  13269  scshwfzeqfzo  13572  rexico  14093  rlim3  14229  rlimclim  14277  caurcvgr  14404  alzdvds  15042  bitsfzolem  15156  pclem  15543  0ram2  15725  0ramcl  15727  symgextfo  17842  lsmless1x  18059  lsmless2x  18060  dprdss  18428  ablfac2  18488  subrgdvds  18794  ssrest  20980  locfincf  21334  fbun  21644  fgss  21677  isucn2  22083  metust  22363  psmetutop  22372  lebnumlem3  22762  lebnum  22763  cfil3i  23067  cfilss  23068  fgcfil  23069  iscau4  23077  ivthle  23225  ivthle2  23226  lhop1lem  23776  lhop2  23778  ply1divex  23896  plyss  23955  dgrlem  23985  elqaa  24077  aannenlem2  24084  reeff1olem  24200  rlimcnp  24692  ftalem3  24801  pntlem3  25298  tgisline  25522  axcontlem2  25845  frgrwopreg1  27182  frgrwopreg2  27183  shless  28218  xlt2addrd  29523  ssnnssfz  29549  xreceu  29630  archirngz  29743  archiabllem1b  29746  locfinreflem  29907  crefss  29916  esumpcvgval  30140  sigaclci  30195  eulerpartlemgvv  30438  eulerpartlemgh  30440  signsply0  30628  iccllysconn  31232  frmin  31739  fgmin  32365  knoppndvlem18  32520  poimirlem26  33435  poimirlem30  33439  volsupnfl  33454  cover2  33508  filbcmb  33535  istotbnd3  33570  sstotbnd  33574  heibor1lem  33608  isdrngo2  33757  isdrngo3  33758  qsss1  34053  islsati  34281  paddss1  35103  paddss2  35104  hdmap14lem2a  37159  pellfundre  37445  pellfundge  37446  pellfundglb  37449  hbtlem3  37697  hbtlem5  37698  itgoss  37733  radcnvrat  38513  fiminre2  39594  uzubico  39795  uzubico2  39797  climleltrp  39908  fourierdlem20  40344  smflimlem2  40980  iccelpart  41369  fmtnofac2  41481  ssnn0ssfz  42127  pgrpgt2nabl  42147