Theorem ssrexv 4006

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 3921	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 631	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1851	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3086	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3086	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1557  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085   ⊆ wss 3904

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086  df-ss 3921

This theorem is referenced by:  ss2rexv  4008  ssn0rex  4310  iunss1  4963  onfr  6381  moriotass  7381  frxp  8101  frfi  9225  fisupcl  9413  supgtoreq  9414  brwdom3  9527  unwdomg  9529  frmin  9704  tcrank  9839  hsmexlem2  10381  pwfseqlem3  10615  grur1  10775  suplem1pr  11007  fimaxre2  12134  fiminre2  12137  suprfinzcl  12684  lbzbi  12934  suprzub  12937  uzsupss  12938  zmin  12942  ssnn0fi  13995  elss2prb  14498  scshwfzeqfzo  14836  rexico  15364  rlim3  15508  rlimclim  15556  caurcvgr  15684  alzdvds  16337  bitsfzolem  16451  pclem  16857  0ram2  17040  0ramcl  17042  symgextfo  19445  lsmless1x  19667  lsmless2x  19668  dprdss  20054  ablfac2  20114  subrgdvds  20615  ssrest  23216  locfincf  23571  fbun  23880  fgss  23913  isucn2  24318  metust  24598  psmetutop  24607  lebnumlem3  25005  lebnum  25006  cfil3i  25311  cfilss  25312  fgcfil  25313  iscau4  25321  ivthle  25498  ivthle2  25499  lhop1lem  26055  lhop2  26057  ply1divex  26177  plyss  26239  dgrlem  26269  elqaa  26363  aannenlem2  26370  reeff1olem  26486  rlimcnp  27007  ftalem3  27116  2sqreultblem  27489  2sqreunnlem1  27490  2sqreunnltblem  27492  pntlem3  27650  madess  27936  addsuniflem  28071  mulsuniflem  28219  tgisline  28773  axcontlem2  29112  frgrwopreg1  30466  frgrwopreg2  30467  shless  31508  xlt2addrd  32911  ssnnssfz  32939  xreceu  33060  archirngz  33330  archiabllem1b  33333  1arithidom  33694  dfufd2lem  33706  locfinreflem  34098  crefss  34107  esumpcvgval  34336  sigaclci  34390  eulerpartlemgvv  34634  eulerpartlemgh  34636  signsply0  34809  iccllysconn  35564  satfvsucsuc  35679  fgmin  36694  knoppndvlem18  36931  poimirlem26  38109  poimirlem30  38113  volsupnfl  38128  cover2  38178  filbcmb  38203  istotbnd3  38234  sstotbnd  38238  heibor1lem  38272  isdrngo2  38421  isdrngo3  38422  qsss1  38758  islsati  39582  paddss1  40405  paddss2  40406  hdmap14lem2a  42455  prjspreln0  43155  pellfundre  43422  pellfundge  43423  pellfundglb  43426  hbtlem3  43668  hbtlem5  43669  itgoss  43704  radcnvrat  44854  uzubico  46106  uzubico2  46108  climleltrp  46214  fourierdlem20  46665  smflimlem2  47310  nndivides2  47942  iccelpart  48003  fmtnofac2  48142  grtriprop  48527  ssnn0ssfz  48935  pgrpgt2nabl  48952  eenglngeehlnmlem1  49323