Theorem ssrexv 4009

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 3924	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1855	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1561  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090  df-ss 3924

This theorem is referenced by:  ss2rexv  4011  ssn0rex  4314  iunss1  4967  onfr  6389  moriotass  7389  frxp  8110  frfi  9233  fisupcl  9418  supgtoreq  9419  brwdom3  9532  unwdomg  9534  frmin  9709  tcrank  9844  hsmexlem2  10399  pwfseqlem3  10633  grur1  10793  suplem1pr  11025  fimaxre2  12151  fiminre2  12154  suprfinzcl  12701  lbzbi  12951  suprzub  12954  uzsupss  12955  zmin  12959  ssnn0fi  14012  elss2prb  14515  scshwfzeqfzo  14853  rexico  15395  rlim3  15539  rlimclim  15587  caurcvgr  15715  alzdvds  16368  bitsfzolem  16482  pclem  16888  0ram2  17071  0ramcl  17073  symgextfo  19483  lsmless1x  19705  lsmless2x  19706  dprdss  20092  ablfac2  20152  subrgdvds  20662  ssrest  23294  locfincf  23649  fbun  23958  fgss  23991  isucn2  24396  metust  24676  psmetutop  24685  lebnumlem3  25083  lebnum  25084  cfil3i  25389  cfilss  25390  fgcfil  25391  iscau4  25399  ivthle  25576  ivthle2  25577  lhop1lem  26133  lhop2  26135  ply1divex  26255  plyss  26317  dgrlem  26347  elqaa  26444  aannenlem2  26451  reeff1olem  26567  rlimcnp  27088  ftalem3  27197  2sqreultblem  27570  2sqreunnlem1  27571  2sqreunnltblem  27573  pntlem3  27731  madess  28017  addsuniflem  28152  mulsuniflem  28300  tgisline  28854  axcontlem2  29224  frgrwopreg1  30578  frgrwopreg2  30579  shless  31620  xlt2addrd  33016  ssnnssfz  33044  xreceu  33154  archirngz  33422  archiabllem1b  33425  1arithidom  33744  dfufd2lem  33756  locfinreflem  34147  crefss  34156  esumpcvgval  34385  sigaclci  34439  eulerpartlemgvv  34683  eulerpartlemgh  34685  signsply0  34855  iccllysconn  35613  satfvsucsuc  35728  fgmin  36743  knoppndvlem18  36980  poimirlem26  38157  poimirlem30  38161  volsupnfl  38176  cover2  38226  filbcmb  38251  istotbnd3  38282  sstotbnd  38286  heibor1lem  38320  isdrngo2  38469  isdrngo3  38470  qsss1  38806  islsati  39630  paddss1  40453  paddss2  40454  hdmap14lem2a  42503  prjspreln0  43203  pellfundre  43470  pellfundge  43471  pellfundglb  43474  hbtlem3  43716  hbtlem5  43717  itgoss  43752  radcnvrat  44888  uzubico  46140  uzubico2  46142  climleltrp  46248  fourierdlem20  46699  smflimlem2  47344  nndivides2  47976  iccelpart  48037  fmtnofac2  48176  grtriprop  48561  ssnn0ssfz  48980  pgrpgt2nabl  48997  eenglngeehlnmlem1  49368