Theorem ssrexv 4001

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 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3088	. . 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 3087   ⊆ wss 3899

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 3088  df-ss 3916

This theorem is used by:  ss2rexv  4003  ssn0rex  4306  iunss1  4966  onfr  6395  moriotass  7401  frxp  8127  frfi  9260  fisupcl  9446  supgtoreq  9447  brwdom3  9560  unwdomg  9562  frmin  9737  tcrank  9882  hsmexlem2  10486  pwfseqlem3  10726  grur1  10886  suplem1pr  11118  fimaxre2  12243  fiminre2  12246  suprfinzcl  12794  lbzbi  13044  suprzub  13047  uzsupss  13048  zmin  13052  ssnn0fi  14108  elss2prb  14613  scshwfzeqfzo  14957  rexico  15501  rlim3  15645  rlimclim  15693  caurcvgr  15821  alzdvds  16470  bitsfzolem  16584  pclem  16996  0ram2  17179  0ramcl  17181  symgextfo  19616  lsmless1x  19838  lsmless2x  19839  dprdss  20225  ablfac2  20285  subrgdvds  20818  isdrng3lem2  20986  isdrng5  20988  ssrest  23474  locfincf  23830  fbun  24139  fgss  24172  isucn2  24577  metust  24857  psmetutop  24866  lebnumlem3  25264  lebnum  25265  cfil3i  25570  cfilss  25571  fgcfil  25572  iscau4  25580  ivthle  25757  ivthle2  25758  lhop1lem  26313  lhop2  26315  ply1divex  26435  plyss  26497  dgrlem  26528  elqaa  26627  aannenlem2  26638  reeff1olem  26755  rlimcnp  27275  ftalem3  27384  2sqreultblem  27757  2sqreunnlem1  27758  2sqreunnltblem  27760  pntlem3  27918  madess  28234  addsuniflem  28369  mulsuniflem  28517  tgisline  29077  axcontlem2  29525  frgrwopreg1  30901  frgrwopreg2  30902  shless  31943  xlt2addrd  33333  ssnnssfz  33361  xreceu  33470  archirngz  33732  archiabllem1b  33735  1arithidom  34051  dfufd2lem  34063  locfinreflem  34454  crefss  34463  esumpcvgval  34692  sigaclci  34746  eulerpartlemgvv  34991  eulerpartlemgh  34993  signsply0  35163  iccllysconn  35984  satfvsucsuc  36099  fgmin  37128  knoppndvlem18  37365  poimirlem26  38532  poimirlem30  38536  volsupnfl  38551  dfprop2  38614  cover2  38617  filbcmb  38642  istotbnd3  38673  sstotbnd  38677  heibor1lem  38711  isdrngo2  38860  isdrngo3  38861  qsss1  39195  islsati  40019  paddss1  40842  paddss2  40843  hdmap14lem2a  42892  prjspreln0  43599  pellfundre  43841  pellfundge  43842  pellfundglb  43845  hbtlem3  44087  hbtlem5  44088  itgoss  44123  radcnvrat  45257  uzubico  46522  uzubico2  46524  climleltrp  46630  fourierdlem20  47081  smflimlem2  47726  nndivides2  48398  iccelpart  48459  fmtnofac2  48598  grtriprop  48983  ssnn0ssfz  49405  pgrpgt2nabl  49422  eenglngeehlnmlem1  49793