Theorem ssrexv 4005

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 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 623	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063  df-ss 3920

This theorem is referenced by:  ss2rexv  4007  ssn0rex  4312  iunss1  4963  onfr  6364  moriotass  7357  frxp  8078  frfi  9197  fisupcl  9385  supgtoreq  9386  brwdom3  9499  unwdomg  9501  frmin  9673  tcrank  9808  hsmexlem2  10349  pwfseqlem3  10583  grur1  10743  suplem1pr  10975  fimaxre2  12099  fiminre2  12102  suprfinzcl  12618  lbzbi  12861  suprzub  12864  uzsupss  12865  zmin  12869  ssnn0fi  13920  elss2prb  14423  scshwfzeqfzo  14761  rexico  15289  rlim3  15433  rlimclim  15481  caurcvgr  15609  alzdvds  16259  bitsfzolem  16373  pclem  16778  0ram2  16961  0ramcl  16963  symgextfo  19363  lsmless1x  19585  lsmless2x  19586  dprdss  19972  ablfac2  20032  subrgdvds  20531  ssrest  23132  locfincf  23487  fbun  23796  fgss  23829  isucn2  24234  metust  24514  psmetutop  24523  lebnumlem3  24930  lebnum  24931  cfil3i  25237  cfilss  25238  fgcfil  25239  iscau4  25247  ivthle  25425  ivthle2  25426  lhop1lem  25986  lhop2  25988  ply1divex  26110  plyss  26172  dgrlem  26202  elqaa  26298  aannenlem2  26305  reeff1olem  26424  rlimcnp  26943  ftalem3  27053  2sqreultblem  27427  2sqreunnlem1  27428  2sqreunnltblem  27430  pntlem3  27588  madess  27874  addsuniflem  28009  mulsuniflem  28157  tgisline  28711  axcontlem2  29050  frgrwopreg1  30405  frgrwopreg2  30406  shless  31446  xlt2addrd  32849  ssnnssfz  32877  xreceu  33013  archirngz  33282  archiabllem1b  33285  1arithidom  33629  dfufd2lem  33641  locfinreflem  34017  crefss  34026  esumpcvgval  34255  sigaclci  34309  eulerpartlemgvv  34553  eulerpartlemgh  34555  signsply0  34728  iccllysconn  35463  satfvsucsuc  35578  fgmin  36583  knoppndvlem18  36748  poimirlem26  37891  poimirlem30  37895  volsupnfl  37910  cover2  37960  filbcmb  37985  istotbnd3  38016  sstotbnd  38020  heibor1lem  38054  isdrngo2  38203  isdrngo3  38204  qsss1  38540  islsati  39364  paddss1  40187  paddss2  40188  hdmap14lem2a  42237  prjspreln0  42961  pellfundre  43232  pellfundge  43233  pellfundglb  43236  hbtlem3  43478  hbtlem5  43479  itgoss  43514  radcnvrat  44664  uzubico  45920  uzubico2  45922  climleltrp  46028  fourierdlem20  46479  smflimlem2  47124  iccelpart  47787  fmtnofac2  47923  grtriprop  48295  ssnn0ssfz  48703  pgrpgt2nabl  48720  eenglngeehlnmlem1  49091