Theorem ssrexv 4008

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 3923	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1862	. . 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 1568  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089   ⊆ wss 3906

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

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

This theorem is referenced by:  ss2rexv  4010  ssn0rex  4314  iunss1  4972  onfr  6402  moriotass  7401  frxp  8123  frfi  9246  fisupcl  9431  supgtoreq  9432  brwdom3  9545  unwdomg  9547  frmin  9722  tcrank  9857  hsmexlem2  10412  pwfseqlem3  10646  grur1  10806  suplem1pr  11038  fimaxre2  12161  fiminre2  12164  suprfinzcl  12711  lbzbi  12961  suprzub  12964  uzsupss  12965  zmin  12969  ssnn0fi  14023  elss2prb  14527  scshwfzeqfzo  14865  rexico  15407  rlim3  15551  rlimclim  15599  caurcvgr  15727  alzdvds  16379  bitsfzolem  16493  pclem  16899  0ram2  17082  0ramcl  17084  symgextfo  19493  lsmless1x  19715  lsmless2x  19716  dprdss  20102  ablfac2  20162  subrgdvds  20672  ssrest  23314  locfincf  23669  fbun  23978  fgss  24011  isucn2  24416  metust  24696  psmetutop  24705  lebnumlem3  25103  lebnum  25104  cfil3i  25409  cfilss  25410  fgcfil  25411  iscau4  25419  ivthle  25596  ivthle2  25597  lhop1lem  26153  lhop2  26155  ply1divex  26275  plyss  26337  dgrlem  26367  elqaa  26464  aannenlem2  26471  reeff1olem  26587  rlimcnp  27108  ftalem3  27217  2sqreultblem  27590  2sqreunnlem1  27591  2sqreunnltblem  27593  pntlem3  27751  madess  28037  addsuniflem  28172  mulsuniflem  28320  tgisline  28878  axcontlem2  29293  frgrwopreg1  30647  frgrwopreg2  30648  shless  31689  xlt2addrd  33082  ssnnssfz  33110  xreceu  33219  archirngz  33487  archiabllem1b  33490  1arithidom  33805  dfufd2lem  33817  locfinreflem  34208  crefss  34217  esumpcvgval  34446  sigaclci  34500  eulerpartlemgvv  34744  eulerpartlemgh  34746  signsply0  34916  iccllysconn  35720  satfvsucsuc  35835  fgmin  36859  knoppndvlem18  37096  poimirlem26  38275  poimirlem30  38279  volsupnfl  38294  cover2  38344  filbcmb  38369  istotbnd3  38400  sstotbnd  38404  heibor1lem  38438  isdrngo2  38587  isdrngo3  38588  qsss1  38922  islsati  39746  paddss1  40569  paddss2  40570  hdmap14lem2a  42619  prjspreln0  43321  pellfundre  43588  pellfundge  43589  pellfundglb  43592  hbtlem3  43834  hbtlem5  43835  itgoss  43870  radcnvrat  45004  uzubico  46262  uzubico2  46264  climleltrp  46370  fourierdlem20  46821  smflimlem2  47466  nndivides2  48098  iccelpart  48159  fmtnofac2  48298  grtriprop  48683  ssnn0ssfz  49106  pgrpgt2nabl  49123  eenglngeehlnmlem1  49494