Theorem ssrexv 3630

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∃wrex 2897   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rex 2902  df-in 3547  df-ss 3554

This theorem is referenced by:  iunss1  4468  onfr  5680  moriotass  6539  frxp  7174  frfi  8090  fisupcl  8258  supgtoreq  8259  brwdom3  8370  unwdomg  8372  tcrank  8630  hsmexlem2  9132  pwfseqlem3  9361  grur1  9521  suplem1pr  9753  fimaxre2  10848  suprfinzcl  11368  lbzbi  11652  suprzub  11655  uzsupss  11656  zmin  11660  ssnn0fi  12646  elss2prb  13123  scshwfzeqfzo  13423  rexico  13941  rlim3  14077  rlimclim  14125  caurcvgr  14252  alzdvds  14880  bitsfzolem  14994  pclem  15381  0ram2  15563  0ramcl  15565  symgextfo  17665  lsmless1x  17882  lsmless2x  17883  dprdss  18251  ablfac2  18311  subrgdvds  18617  ssrest  20790  locfincf  21144  fbun  21454  fgss  21487  isucn2  21893  metust  22173  psmetutop  22182  lebnumlem3  22570  lebnum  22571  cfil3i  22875  cfilss  22876  fgcfil  22877  iscau4  22885  ivthle  23032  ivthle2  23033  lhop1lem  23580  lhop2  23582  ply1divex  23700  plyss  23759  dgrlem  23789  elqaa  23881  aannenlem2  23888  reeff1olem  24004  rlimcnp  24492  ftalem3  24601  pntlem3  25098  tgisline  25322  axcontlem2  25645  frgrawopreg1  26577  frgrawopreg2  26578  shless  27602  xlt2addrd  28913  ssnnssfz  28937  xreceu  28961  archirngz  29074  archiabllem1b  29077  locfinreflem  29235  crefss  29244  esumpcvgval  29467  sigaclci  29522  eulerpartlemgvv  29765  eulerpartlemgh  29767  signsply0  29954  iccllyscon  30486  frmin  30983  nodenselem4  31083  fgmin  31535  knoppndvlem18  31690  poimirlem26  32605  poimirlem30  32609  volsupnfl  32624  cover2  32678  filbcmb  32705  istotbnd3  32740  sstotbnd  32744  heibor1lem  32778  isdrngo2  32927  isdrngo3  32928  islsati  33299  paddss1  34121  paddss2  34122  hdmap14lem2a  36177  pellfundre  36463  pellfundge  36464  pellfundglb  36467  hbtlem3  36716  hbtlem5  36717  itgoss  36752  radcnvrat  37535  fiminre2  38535  climleltrp  38743  fourierdlem20  39020  smflimlem2  39658  iccelpart  39971  fmtnofac2  40019  ssn0rex  40311  frgrwopreg1  41487  frgrwopreg2  41488  ssnn0ssfz  41920  pgrpgt2nabl  41941