Theorem ssrexv 4033

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109  ∃wrex 3061   ⊆ wss 3931

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3062  df-ss 3948

This theorem is referenced by:  ss2rexv  4035  ssn0rex  4338  iunss1  4987  onfr  6396  moriotass  7399  frxp  8130  frfi  9298  fisupcl  9487  supgtoreq  9488  brwdom3  9601  unwdomg  9603  frmin  9768  tcrank  9903  hsmexlem2  10446  pwfseqlem3  10679  grur1  10839  suplem1pr  11071  fimaxre2  12192  fiminre2  12195  suprfinzcl  12712  lbzbi  12957  suprzub  12960  uzsupss  12961  zmin  12965  ssnn0fi  14008  elss2prb  14511  scshwfzeqfzo  14850  rexico  15377  rlim3  15519  rlimclim  15567  caurcvgr  15695  alzdvds  16344  bitsfzolem  16458  pclem  16863  0ram2  17046  0ramcl  17048  symgextfo  19408  lsmless1x  19630  lsmless2x  19631  dprdss  20017  ablfac2  20077  subrgdvds  20551  ssrest  23119  locfincf  23474  fbun  23783  fgss  23816  isucn2  24222  metust  24502  psmetutop  24511  lebnumlem3  24918  lebnum  24919  cfil3i  25226  cfilss  25227  fgcfil  25228  iscau4  25236  ivthle  25414  ivthle2  25415  lhop1lem  25975  lhop2  25977  ply1divex  26099  plyss  26161  dgrlem  26191  elqaa  26287  aannenlem2  26294  reeff1olem  26413  rlimcnp  26932  ftalem3  27042  2sqreultblem  27416  2sqreunnlem1  27417  2sqreunnltblem  27419  pntlem3  27577  madess  27845  addsuniflem  27965  mulsuniflem  28109  tgisline  28611  axcontlem2  28949  frgrwopreg1  30304  frgrwopreg2  30305  shless  31345  xlt2addrd  32741  ssnnssfz  32769  xreceu  32901  archirngz  33192  archiabllem1b  33195  1arithidom  33557  dfufd2lem  33569  locfinreflem  33876  crefss  33885  esumpcvgval  34114  sigaclci  34168  eulerpartlemgvv  34413  eulerpartlemgh  34415  signsply0  34588  iccllysconn  35277  satfvsucsuc  35392  fgmin  36393  knoppndvlem18  36552  poimirlem26  37675  poimirlem30  37679  volsupnfl  37694  cover2  37744  filbcmb  37769  istotbnd3  37800  sstotbnd  37804  heibor1lem  37838  isdrngo2  37987  isdrngo3  37988  qsss1  38312  islsati  39017  paddss1  39841  paddss2  39842  hdmap14lem2a  41891  prjspreln0  42607  pellfundre  42879  pellfundge  42880  pellfundglb  42883  hbtlem3  43126  hbtlem5  43127  itgoss  43162  radcnvrat  44313  uzubico  45575  uzubico2  45577  climleltrp  45685  fourierdlem20  46136  smflimlem2  46781  iccelpart  47427  fmtnofac2  47563  grtriprop  47933  ssnn0ssfz  48304  pgrpgt2nabl  48321  eenglngeehlnmlem1  48697