Theorem ssrexv 3999

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087   ⊆ wss 3914

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088  df-ss 3915

This theorem is used by:  ss2rexv  4001  ssn0rex  4306  iunss1  4966  onfr  6403  moriotass  7410  frxp  8139  frfi  9277  fisupcl  9463  supgtoreq  9464  brwdom3  9577  unwdomg  9579  frmin  9754  tcrank  9902  hsmexlem2  10506  pwfseqlem3  10746  grur1  10906  suplem1pr  11138  fimaxre2  12263  fiminre2  12266  suprfinzcl  12814  lbzbi  13064  suprzub  13067  uzsupss  13068  zmin  13072  ssnn0fi  14129  elss2prb  14634  scshwfzeqfzo  14978  rexico  15522  rlim3  15666  rlimclim  15714  caurcvgr  15842  alzdvds  16491  bitsfzolem  16605  pclem  17017  0ram2  17200  0ramcl  17202  symgextfo  19637  lsmless1x  19859  lsmless2x  19860  dprdss  20246  ablfac2  20306  subrgdvds  20839  isdrng3lem2  21007  isdrng5  21009  ssrest  23495  locfincf  23851  fbun  24160  fgss  24193  isucn2  24598  metust  24878  psmetutop  24887  lebnumlem3  25285  lebnum  25286  cfil3i  25591  cfilss  25592  fgcfil  25593  iscau4  25601  ivthle  25778  ivthle2  25779  lhop1lem  26334  lhop2  26336  ply1divex  26456  plyss  26518  dgrlem  26549  elqaa  26646  aannenlem2  26657  reeff1olem  26774  rlimcnp  27294  ftalem3  27403  2sqreultblem  27776  2sqreunnlem1  27777  2sqreunnltblem  27779  pntlem3  27937  madess  28253  addsuniflem  28388  mulsuniflem  28536  tgisline  29096  axcontlem2  29544  frgrwopreg1  30920  frgrwopreg2  30921  shless  31962  xlt2addrd  33352  ssnnssfz  33380  xreceu  33489  archirngz  33751  archiabllem1b  33754  1arithidom  34070  dfufd2lem  34082  locfinreflem  34473  crefss  34482  esumpcvgval  34711  sigaclci  34765  eulerpartlemgvv  35009  eulerpartlemgh  35011  signsply0  35181  iccllysconn  36016  satfvsucsuc  36131  fgmin  37159  knoppndvlem18  37396  poimirlem26  38566  poimirlem30  38570  volsupnfl  38585  dfprop2  38648  cover2  38651  filbcmb  38676  istotbnd3  38707  sstotbnd  38711  heibor1lem  38745  isdrngo2  38894  isdrngo3  38895  qsss1  39229  islsati  40053  paddss1  40876  paddss2  40877  hdmap14lem2a  42926  prjspreln0  43639  pellfundre  43889  pellfundge  43890  pellfundglb  43893  hbtlem3  44130  hbtlem5  44131  itgoss  44166  radcnvrat  45299  uzubico  46579  uzubico2  46581  climleltrp  46687  fourierdlem20  47138  smflimlem2  47783  nndivides2  48455  iccelpart  48516  fmtnofac2  48655  grtriprop  49040  ssnn0ssfz  49462  pgrpgt2nabl  49479  eenglngeehlnmlem1  49850