Theorem ssrexv 4078

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076   ⊆ wss 3976

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077  df-ss 3993

This theorem is referenced by:  ss2rexv  4080  ssn0rex  4381  iunss1  5029  onfr  6434  moriotass  7437  frxp  8167  frfi  9349  fisupcl  9538  supgtoreq  9539  brwdom3  9651  unwdomg  9653  frmin  9818  tcrank  9953  hsmexlem2  10496  pwfseqlem3  10729  grur1  10889  suplem1pr  11121  fimaxre2  12240  fiminre2  12243  suprfinzcl  12757  lbzbi  13001  suprzub  13004  uzsupss  13005  zmin  13009  ssnn0fi  14036  elss2prb  14537  scshwfzeqfzo  14875  rexico  15402  rlim3  15544  rlimclim  15592  caurcvgr  15722  alzdvds  16368  bitsfzolem  16480  pclem  16885  0ram2  17068  0ramcl  17070  symgextfo  19464  lsmless1x  19686  lsmless2x  19687  dprdss  20073  ablfac2  20133  subrgdvds  20614  ssrest  23205  locfincf  23560  fbun  23869  fgss  23902  isucn2  24309  metust  24592  psmetutop  24601  lebnumlem3  25014  lebnum  25015  cfil3i  25322  cfilss  25323  fgcfil  25324  iscau4  25332  ivthle  25510  ivthle2  25511  lhop1lem  26072  lhop2  26074  ply1divex  26196  plyss  26258  dgrlem  26288  elqaa  26382  aannenlem2  26389  reeff1olem  26508  rlimcnp  27026  ftalem3  27136  2sqreultblem  27510  2sqreunnlem1  27511  2sqreunnltblem  27513  pntlem3  27671  madess  27933  addsuniflem  28052  mulsuniflem  28193  tgisline  28653  axcontlem2  28998  frgrwopreg1  30350  frgrwopreg2  30351  shless  31391  xlt2addrd  32765  ssnnssfz  32792  xreceu  32886  archirngz  33169  archiabllem1b  33172  1arithidom  33530  dfufd2lem  33542  locfinreflem  33786  crefss  33795  esumpcvgval  34042  sigaclci  34096  eulerpartlemgvv  34341  eulerpartlemgh  34343  signsply0  34528  iccllysconn  35218  satfvsucsuc  35333  fgmin  36336  knoppndvlem18  36495  poimirlem26  37606  poimirlem30  37610  volsupnfl  37625  cover2  37675  filbcmb  37700  istotbnd3  37731  sstotbnd  37735  heibor1lem  37769  isdrngo2  37918  isdrngo3  37919  qsss1  38245  islsati  38950  paddss1  39774  paddss2  39775  hdmap14lem2a  41824  prjspreln0  42564  pellfundre  42837  pellfundge  42838  pellfundglb  42841  hbtlem3  43084  hbtlem5  43085  itgoss  43120  radcnvrat  44283  uzubico  45486  uzubico2  45488  climleltrp  45597  fourierdlem20  46048  smflimlem2  46693  iccelpart  47307  fmtnofac2  47443  grtriprop  47792  ssnn0ssfz  48074  pgrpgt2nabl  48091  eenglngeehlnmlem1  48471