Theorem ssrexv 3992

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063  df-ss 3907

This theorem is referenced by:  ss2rexv  3994  ssn0rex  4299  iunss1  4949  onfr  6356  moriotass  7349  frxp  8069  frfi  9188  fisupcl  9376  supgtoreq  9377  brwdom3  9490  unwdomg  9492  frmin  9664  tcrank  9799  hsmexlem2  10340  pwfseqlem3  10574  grur1  10734  suplem1pr  10966  fimaxre2  12092  fiminre2  12095  suprfinzcl  12634  lbzbi  12877  suprzub  12880  uzsupss  12881  zmin  12885  ssnn0fi  13938  elss2prb  14441  scshwfzeqfzo  14779  rexico  15307  rlim3  15451  rlimclim  15499  caurcvgr  15627  alzdvds  16280  bitsfzolem  16394  pclem  16800  0ram2  16983  0ramcl  16985  symgextfo  19388  lsmless1x  19610  lsmless2x  19611  dprdss  19997  ablfac2  20057  subrgdvds  20554  ssrest  23151  locfincf  23506  fbun  23815  fgss  23848  isucn2  24253  metust  24533  psmetutop  24542  lebnumlem3  24940  lebnum  24941  cfil3i  25246  cfilss  25247  fgcfil  25248  iscau4  25256  ivthle  25433  ivthle2  25434  lhop1lem  25990  lhop2  25992  ply1divex  26112  plyss  26174  dgrlem  26204  elqaa  26299  aannenlem2  26306  reeff1olem  26424  rlimcnp  26942  ftalem3  27052  2sqreultblem  27425  2sqreunnlem1  27426  2sqreunnltblem  27428  pntlem3  27586  madess  27872  addsuniflem  28007  mulsuniflem  28155  tgisline  28709  axcontlem2  29048  frgrwopreg1  30403  frgrwopreg2  30404  shless  31445  xlt2addrd  32847  ssnnssfz  32875  xreceu  32996  archirngz  33265  archiabllem1b  33268  1arithidom  33612  dfufd2lem  33624  locfinreflem  34000  crefss  34009  esumpcvgval  34238  sigaclci  34292  eulerpartlemgvv  34536  eulerpartlemgh  34538  signsply0  34711  iccllysconn  35448  satfvsucsuc  35563  fgmin  36568  knoppndvlem18  36805  poimirlem26  37981  poimirlem30  37985  volsupnfl  38000  cover2  38050  filbcmb  38075  istotbnd3  38106  sstotbnd  38110  heibor1lem  38144  isdrngo2  38293  isdrngo3  38294  qsss1  38630  islsati  39454  paddss1  40277  paddss2  40278  hdmap14lem2a  42327  prjspreln0  43056  pellfundre  43327  pellfundge  43328  pellfundglb  43331  hbtlem3  43573  hbtlem5  43574  itgoss  43609  radcnvrat  44759  uzubico  46014  uzubico2  46016  climleltrp  46122  fourierdlem20  46573  smflimlem2  47218  nndivides2  47844  iccelpart  47905  fmtnofac2  48044  grtriprop  48429  ssnn0ssfz  48837  pgrpgt2nabl  48854  eenglngeehlnmlem1  49225