Theorem ssrexv 4007

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 3922	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 622	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1832	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3054	. . 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 3053   ⊆ wss 3905

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 3054  df-ss 3922

This theorem is referenced by:  ss2rexv  4009  ssn0rex  4311  iunss1  4959  onfr  6350  moriotass  7342  frxp  8066  frfi  9190  fisupcl  9379  supgtoreq  9380  brwdom3  9493  unwdomg  9495  frmin  9664  tcrank  9799  hsmexlem2  10340  pwfseqlem3  10573  grur1  10733  suplem1pr  10965  fimaxre2  12088  fiminre2  12091  suprfinzcl  12608  lbzbi  12855  suprzub  12858  uzsupss  12859  zmin  12863  ssnn0fi  13910  elss2prb  14413  scshwfzeqfzo  14751  rexico  15279  rlim3  15423  rlimclim  15471  caurcvgr  15599  alzdvds  16249  bitsfzolem  16363  pclem  16768  0ram2  16951  0ramcl  16953  symgextfo  19319  lsmless1x  19541  lsmless2x  19542  dprdss  19928  ablfac2  19988  subrgdvds  20489  ssrest  23079  locfincf  23434  fbun  23743  fgss  23776  isucn2  24182  metust  24462  psmetutop  24471  lebnumlem3  24878  lebnum  24879  cfil3i  25185  cfilss  25186  fgcfil  25187  iscau4  25195  ivthle  25373  ivthle2  25374  lhop1lem  25934  lhop2  25936  ply1divex  26058  plyss  26120  dgrlem  26150  elqaa  26246  aannenlem2  26253  reeff1olem  26372  rlimcnp  26891  ftalem3  27001  2sqreultblem  27375  2sqreunnlem1  27376  2sqreunnltblem  27378  pntlem3  27536  madess  27808  addsuniflem  27931  mulsuniflem  28075  tgisline  28590  axcontlem2  28928  frgrwopreg1  30280  frgrwopreg2  30281  shless  31321  xlt2addrd  32715  ssnnssfz  32743  xreceu  32875  archirngz  33141  archiabllem1b  33144  1arithidom  33484  dfufd2lem  33496  locfinreflem  33806  crefss  33815  esumpcvgval  34044  sigaclci  34098  eulerpartlemgvv  34343  eulerpartlemgh  34345  signsply0  34518  iccllysconn  35222  satfvsucsuc  35337  fgmin  36343  knoppndvlem18  36502  poimirlem26  37625  poimirlem30  37629  volsupnfl  37644  cover2  37694  filbcmb  37719  istotbnd3  37750  sstotbnd  37754  heibor1lem  37788  isdrngo2  37937  isdrngo3  37938  qsss1  38262  islsati  38972  paddss1  39796  paddss2  39797  hdmap14lem2a  41846  prjspreln0  42582  pellfundre  42854  pellfundge  42855  pellfundglb  42858  hbtlem3  43100  hbtlem5  43101  itgoss  43136  radcnvrat  44287  uzubico  45548  uzubico2  45550  climleltrp  45658  fourierdlem20  46109  smflimlem2  46754  iccelpart  47418  fmtnofac2  47554  grtriprop  47926  ssnn0ssfz  48334  pgrpgt2nabl  48351  eenglngeehlnmlem1  48723