Theorem ssrexv 4000

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 622	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3058	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3058	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057   ⊆ wss 3898

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058  df-ss 3915

This theorem is referenced by:  ss2rexv  4002  ssn0rex  4307  iunss1  4956  onfr  6350  moriotass  7341  frxp  8062  frfi  9176  fisupcl  9361  supgtoreq  9362  brwdom3  9475  unwdomg  9477  frmin  9649  tcrank  9784  hsmexlem2  10325  pwfseqlem3  10558  grur1  10718  suplem1pr  10950  fimaxre2  12074  fiminre2  12077  suprfinzcl  12593  lbzbi  12836  suprzub  12839  uzsupss  12840  zmin  12844  ssnn0fi  13894  elss2prb  14397  scshwfzeqfzo  14735  rexico  15263  rlim3  15407  rlimclim  15455  caurcvgr  15583  alzdvds  16233  bitsfzolem  16347  pclem  16752  0ram2  16935  0ramcl  16937  symgextfo  19336  lsmless1x  19558  lsmless2x  19559  dprdss  19945  ablfac2  20005  subrgdvds  20503  ssrest  23092  locfincf  23447  fbun  23756  fgss  23789  isucn2  24194  metust  24474  psmetutop  24483  lebnumlem3  24890  lebnum  24891  cfil3i  25197  cfilss  25198  fgcfil  25199  iscau4  25207  ivthle  25385  ivthle2  25386  lhop1lem  25946  lhop2  25948  ply1divex  26070  plyss  26132  dgrlem  26162  elqaa  26258  aannenlem2  26265  reeff1olem  26384  rlimcnp  26903  ftalem3  27013  2sqreultblem  27387  2sqreunnlem1  27388  2sqreunnltblem  27390  pntlem3  27548  madess  27822  addsuniflem  27945  mulsuniflem  28089  tgisline  28606  axcontlem2  28945  frgrwopreg1  30300  frgrwopreg2  30301  shless  31341  xlt2addrd  32746  ssnnssfz  32774  xreceu  32909  archirngz  33165  archiabllem1b  33168  1arithidom  33509  dfufd2lem  33521  locfinreflem  33874  crefss  33883  esumpcvgval  34112  sigaclci  34166  eulerpartlemgvv  34410  eulerpartlemgh  34412  signsply0  34585  iccllysconn  35315  satfvsucsuc  35430  fgmin  36435  knoppndvlem18  36594  poimirlem26  37706  poimirlem30  37710  volsupnfl  37725  cover2  37775  filbcmb  37800  istotbnd3  37831  sstotbnd  37835  heibor1lem  37869  isdrngo2  38018  isdrngo3  38019  qsss1  38347  islsati  39113  paddss1  39936  paddss2  39937  hdmap14lem2a  41986  prjspreln0  42727  pellfundre  42998  pellfundge  42999  pellfundglb  43002  hbtlem3  43244  hbtlem5  43245  itgoss  43280  radcnvrat  44431  uzubico  45690  uzubico2  45692  climleltrp  45798  fourierdlem20  46249  smflimlem2  46894  iccelpart  47557  fmtnofac2  47693  grtriprop  48065  ssnn0ssfz  48473  pgrpgt2nabl  48490  eenglngeehlnmlem1  48862