Theorem ssrexv 3991

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 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 623	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1834	. . 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 1540  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061   ⊆ wss 3889

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 3062  df-ss 3906

This theorem is referenced by:  ss2rexv  3993  ssn0rex  4298  iunss1  4948  onfr  6362  moriotass  7356  frxp  8076  frfi  9195  fisupcl  9383  supgtoreq  9384  brwdom3  9497  unwdomg  9499  frmin  9673  tcrank  9808  hsmexlem2  10349  pwfseqlem3  10583  grur1  10743  suplem1pr  10975  fimaxre2  12101  fiminre2  12104  suprfinzcl  12643  lbzbi  12886  suprzub  12889  uzsupss  12890  zmin  12894  ssnn0fi  13947  elss2prb  14450  scshwfzeqfzo  14788  rexico  15316  rlim3  15460  rlimclim  15508  caurcvgr  15636  alzdvds  16289  bitsfzolem  16403  pclem  16809  0ram2  16992  0ramcl  16994  symgextfo  19397  lsmless1x  19619  lsmless2x  19620  dprdss  20006  ablfac2  20066  subrgdvds  20563  ssrest  23141  locfincf  23496  fbun  23805  fgss  23838  isucn2  24243  metust  24523  psmetutop  24532  lebnumlem3  24930  lebnum  24931  cfil3i  25236  cfilss  25237  fgcfil  25238  iscau4  25246  ivthle  25423  ivthle2  25424  lhop1lem  25980  lhop2  25982  ply1divex  26102  plyss  26164  dgrlem  26194  elqaa  26288  aannenlem2  26295  reeff1olem  26411  rlimcnp  26929  ftalem3  27038  2sqreultblem  27411  2sqreunnlem1  27412  2sqreunnltblem  27414  pntlem3  27572  madess  27858  addsuniflem  27993  mulsuniflem  28141  tgisline  28695  axcontlem2  29034  frgrwopreg1  30388  frgrwopreg2  30389  shless  31430  xlt2addrd  32832  ssnnssfz  32860  xreceu  32981  archirngz  33250  archiabllem1b  33253  1arithidom  33597  dfufd2lem  33609  locfinreflem  33984  crefss  33993  esumpcvgval  34222  sigaclci  34276  eulerpartlemgvv  34520  eulerpartlemgh  34522  signsply0  34695  iccllysconn  35432  satfvsucsuc  35547  fgmin  36552  knoppndvlem18  36789  poimirlem26  37967  poimirlem30  37971  volsupnfl  37986  cover2  38036  filbcmb  38061  istotbnd3  38092  sstotbnd  38096  heibor1lem  38130  isdrngo2  38279  isdrngo3  38280  qsss1  38616  islsati  39440  paddss1  40263  paddss2  40264  hdmap14lem2a  42313  prjspreln0  43042  pellfundre  43309  pellfundge  43310  pellfundglb  43313  hbtlem3  43555  hbtlem5  43556  itgoss  43591  radcnvrat  44741  uzubico  45996  uzubico2  45998  climleltrp  46104  fourierdlem20  46555  smflimlem2  47200  nndivides2  47832  iccelpart  47893  fmtnofac2  48032  grtriprop  48417  ssnn0ssfz  48825  pgrpgt2nabl  48842  eenglngeehlnmlem1  49213