Theorem ssrexv 4016

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053   ⊆ wss 3914

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054  df-ss 3931

This theorem is referenced by:  ss2rexv  4018  ssn0rex  4321  iunss1  4970  onfr  6371  moriotass  7376  frxp  8105  frfi  9232  fisupcl  9421  supgtoreq  9422  brwdom3  9535  unwdomg  9537  frmin  9702  tcrank  9837  hsmexlem2  10380  pwfseqlem3  10613  grur1  10773  suplem1pr  11005  fimaxre2  12128  fiminre2  12131  suprfinzcl  12648  lbzbi  12895  suprzub  12898  uzsupss  12899  zmin  12903  ssnn0fi  13950  elss2prb  14453  scshwfzeqfzo  14792  rexico  15320  rlim3  15464  rlimclim  15512  caurcvgr  15640  alzdvds  16290  bitsfzolem  16404  pclem  16809  0ram2  16992  0ramcl  16994  symgextfo  19352  lsmless1x  19574  lsmless2x  19575  dprdss  19961  ablfac2  20021  subrgdvds  20495  ssrest  23063  locfincf  23418  fbun  23727  fgss  23760  isucn2  24166  metust  24446  psmetutop  24455  lebnumlem3  24862  lebnum  24863  cfil3i  25169  cfilss  25170  fgcfil  25171  iscau4  25179  ivthle  25357  ivthle2  25358  lhop1lem  25918  lhop2  25920  ply1divex  26042  plyss  26104  dgrlem  26134  elqaa  26230  aannenlem2  26237  reeff1olem  26356  rlimcnp  26875  ftalem3  26985  2sqreultblem  27359  2sqreunnlem1  27360  2sqreunnltblem  27362  pntlem3  27520  madess  27788  addsuniflem  27908  mulsuniflem  28052  tgisline  28554  axcontlem2  28892  frgrwopreg1  30247  frgrwopreg2  30248  shless  31288  xlt2addrd  32682  ssnnssfz  32710  xreceu  32842  archirngz  33143  archiabllem1b  33146  1arithidom  33508  dfufd2lem  33520  locfinreflem  33830  crefss  33839  esumpcvgval  34068  sigaclci  34122  eulerpartlemgvv  34367  eulerpartlemgh  34369  signsply0  34542  iccllysconn  35237  satfvsucsuc  35352  fgmin  36358  knoppndvlem18  36517  poimirlem26  37640  poimirlem30  37644  volsupnfl  37659  cover2  37709  filbcmb  37734  istotbnd3  37765  sstotbnd  37769  heibor1lem  37803  isdrngo2  37952  isdrngo3  37953  qsss1  38277  islsati  38987  paddss1  39811  paddss2  39812  hdmap14lem2a  41861  prjspreln0  42597  pellfundre  42869  pellfundge  42870  pellfundglb  42873  hbtlem3  43116  hbtlem5  43117  itgoss  43152  radcnvrat  44303  uzubico  45564  uzubico2  45566  climleltrp  45674  fourierdlem20  46125  smflimlem2  46770  iccelpart  47434  fmtnofac2  47570  grtriprop  47940  ssnn0ssfz  48337  pgrpgt2nabl  48354  eenglngeehlnmlem1  48726