Theorem ssrexv 4003

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 3918	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 622	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3061	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3061	. . 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 3060   ⊆ wss 3901

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 3061  df-ss 3918

This theorem is referenced by:  ss2rexv  4005  ssn0rex  4310  iunss1  4961  onfr  6356  moriotass  7347  frxp  8068  frfi  9185  fisupcl  9373  supgtoreq  9374  brwdom3  9487  unwdomg  9489  frmin  9661  tcrank  9796  hsmexlem2  10337  pwfseqlem3  10571  grur1  10731  suplem1pr  10963  fimaxre2  12087  fiminre2  12090  suprfinzcl  12606  lbzbi  12849  suprzub  12852  uzsupss  12853  zmin  12857  ssnn0fi  13908  elss2prb  14411  scshwfzeqfzo  14749  rexico  15277  rlim3  15421  rlimclim  15469  caurcvgr  15597  alzdvds  16247  bitsfzolem  16361  pclem  16766  0ram2  16949  0ramcl  16951  symgextfo  19351  lsmless1x  19573  lsmless2x  19574  dprdss  19960  ablfac2  20020  subrgdvds  20519  ssrest  23120  locfincf  23475  fbun  23784  fgss  23817  isucn2  24222  metust  24502  psmetutop  24511  lebnumlem3  24918  lebnum  24919  cfil3i  25225  cfilss  25226  fgcfil  25227  iscau4  25235  ivthle  25413  ivthle2  25414  lhop1lem  25974  lhop2  25976  ply1divex  26098  plyss  26160  dgrlem  26190  elqaa  26286  aannenlem2  26293  reeff1olem  26412  rlimcnp  26931  ftalem3  27041  2sqreultblem  27415  2sqreunnlem1  27416  2sqreunnltblem  27418  pntlem3  27576  madess  27862  addsuniflem  27997  mulsuniflem  28145  tgisline  28699  axcontlem2  29038  frgrwopreg1  30393  frgrwopreg2  30394  shless  31434  xlt2addrd  32839  ssnnssfz  32867  xreceu  33003  archirngz  33271  archiabllem1b  33274  1arithidom  33618  dfufd2lem  33630  locfinreflem  33997  crefss  34006  esumpcvgval  34235  sigaclci  34289  eulerpartlemgvv  34533  eulerpartlemgh  34535  signsply0  34708  iccllysconn  35444  satfvsucsuc  35559  fgmin  36564  knoppndvlem18  36729  poimirlem26  37843  poimirlem30  37847  volsupnfl  37862  cover2  37912  filbcmb  37937  istotbnd3  37968  sstotbnd  37972  heibor1lem  38006  isdrngo2  38155  isdrngo3  38156  qsss1  38484  islsati  39250  paddss1  40073  paddss2  40074  hdmap14lem2a  42123  prjspreln0  42848  pellfundre  43119  pellfundge  43120  pellfundglb  43123  hbtlem3  43365  hbtlem5  43366  itgoss  43401  radcnvrat  44551  uzubico  45808  uzubico2  45810  climleltrp  45916  fourierdlem20  46367  smflimlem2  47012  iccelpart  47675  fmtnofac2  47811  grtriprop  48183  ssnn0ssfz  48591  pgrpgt2nabl  48608  eenglngeehlnmlem1  48979