Theorem ssrexv 4004

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.) Avoid axioms. (Revised by GG, 19-May-2025.)

Assertion

Ref	Expression
ssrexv	⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrexv

Step	Hyp	Ref	Expression
1		df-ss 3919	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3089	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3089	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2145  ∃wrex 3088   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089  df-ss 3919

This theorem is used by:  ss2rexv  4006  ssn0rex  4309  iunss1  4969  onfr  6401  moriotass  7406  frxp  8128  frfi  9259  fisupcl  9444  supgtoreq  9445  brwdom3  9558  unwdomg  9560  frmin  9735  tcrank  9870  hsmexlem2  10433  pwfseqlem3  10673  grur1  10833  suplem1pr  11065  fimaxre2  12188  fiminre2  12191  suprfinzcl  12739  lbzbi  12989  suprzub  12992  uzsupss  12993  zmin  12997  ssnn0fi  14053  elss2prb  14557  scshwfzeqfzo  14901  rexico  15445  rlim3  15589  rlimclim  15637  caurcvgr  15765  alzdvds  16416  bitsfzolem  16530  pclem  16936  0ram2  17119  0ramcl  17121  symgextfo  19555  lsmless1x  19777  lsmless2x  19778  dprdss  20164  ablfac2  20224  subrgdvds  20754  isdrng3lem2  20921  isdrng5  20923  ssrest  23407  locfincf  23763  fbun  24072  fgss  24105  isucn2  24510  metust  24790  psmetutop  24799  lebnumlem3  25197  lebnum  25198  cfil3i  25503  cfilss  25504  fgcfil  25505  iscau4  25513  ivthle  25690  ivthle2  25691  lhop1lem  26247  lhop2  26249  ply1divex  26369  plyss  26431  dgrlem  26462  elqaa  26561  aannenlem2  26572  reeff1olem  26689  rlimcnp  27210  ftalem3  27319  2sqreultblem  27692  2sqreunnlem1  27693  2sqreunnltblem  27695  pntlem3  27853  madess  28139  addsuniflem  28274  mulsuniflem  28422  tgisline  28982  axcontlem2  29430  frgrwopreg1  30806  frgrwopreg2  30807  shless  31848  xlt2addrd  33238  ssnnssfz  33266  xreceu  33375  archirngz  33637  archiabllem1b  33640  1arithidom  33955  dfufd2lem  33967  locfinreflem  34358  crefss  34367  esumpcvgval  34596  sigaclci  34650  eulerpartlemgvv  34895  eulerpartlemgh  34897  signsply0  35067  iccllysconn  35837  satfvsucsuc  35952  fgmin  36997  knoppndvlem18  37234  poimirlem26  38403  poimirlem30  38407  volsupnfl  38422  cover2  38473  filbcmb  38498  istotbnd3  38529  sstotbnd  38533  heibor1lem  38567  isdrngo2  38716  isdrngo3  38717  qsss1  39051  islsati  39875  paddss1  40698  paddss2  40699  hdmap14lem2a  42748  prjspreln0  43463  pellfundre  43730  pellfundge  43731  pellfundglb  43734  hbtlem3  43976  hbtlem5  43977  itgoss  44012  radcnvrat  45146  uzubico  46404  uzubico2  46406  climleltrp  46512  fourierdlem20  46963  smflimlem2  47608  nndivides2  48280  iccelpart  48341  fmtnofac2  48480  grtriprop  48865  ssnn0ssfz  49287  pgrpgt2nabl  49304  eenglngeehlnmlem1  49675