Theorem ssrexv 4010

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 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3093	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3093	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2146  ∃wrex 3092   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093  df-ss 3925

This theorem is used by:  ss2rexv  4012  ssn0rex  4316  iunss1  4976  onfr  6407  moriotass  7412  frxp  8131  frfi  9255  fisupcl  9440  supgtoreq  9441  brwdom3  9554  unwdomg  9556  frmin  9731  tcrank  9866  hsmexlem2  10429  pwfseqlem3  10663  grur1  10823  suplem1pr  11055  fimaxre2  12178  fiminre2  12181  suprfinzcl  12728  lbzbi  12978  suprzub  12981  uzsupss  12982  zmin  12986  ssnn0fi  14041  elss2prb  14545  scshwfzeqfzo  14889  rexico  15431  rlim3  15575  rlimclim  15623  caurcvgr  15751  alzdvds  16403  bitsfzolem  16517  pclem  16923  0ram2  17106  0ramcl  17108  symgextfo  19523  lsmless1x  19745  lsmless2x  19746  dprdss  20132  ablfac2  20192  subrgdvds  20722  isdrng3lem2  20889  isdrng5  20891  ssrest  23370  locfincf  23725  fbun  24034  fgss  24067  isucn2  24472  metust  24752  psmetutop  24761  lebnumlem3  25159  lebnum  25160  cfil3i  25465  cfilss  25466  fgcfil  25467  iscau4  25475  ivthle  25652  ivthle2  25653  lhop1lem  26209  lhop2  26211  ply1divex  26331  plyss  26393  dgrlem  26423  elqaa  26520  aannenlem2  26529  reeff1olem  26646  rlimcnp  27167  ftalem3  27276  2sqreultblem  27649  2sqreunnlem1  27650  2sqreunnltblem  27652  pntlem3  27810  madess  28096  addsuniflem  28231  mulsuniflem  28379  tgisline  28937  axcontlem2  29352  frgrwopreg1  30706  frgrwopreg2  30707  shless  31748  xlt2addrd  33141  ssnnssfz  33169  xreceu  33278  archirngz  33540  archiabllem1b  33543  1arithidom  33858  dfufd2lem  33870  locfinreflem  34261  crefss  34270  esumpcvgval  34499  sigaclci  34553  eulerpartlemgvv  34797  eulerpartlemgh  34799  signsply0  34969  iccllysconn  35762  satfvsucsuc  35877  fgmin  36921  knoppndvlem18  37158  poimirlem26  38337  poimirlem30  38341  volsupnfl  38356  cover2  38406  filbcmb  38431  istotbnd3  38462  sstotbnd  38466  heibor1lem  38500  isdrngo2  38649  isdrngo3  38650  qsss1  38984  islsati  39808  paddss1  40631  paddss2  40632  hdmap14lem2a  42681  prjspreln0  43381  pellfundre  43648  pellfundge  43649  pellfundglb  43652  hbtlem3  43894  hbtlem5  43895  itgoss  43930  radcnvrat  45064  uzubico  46322  uzubico2  46324  climleltrp  46430  fourierdlem20  46881  smflimlem2  47526  nndivides2  48161  iccelpart  48222  fmtnofac2  48361  grtriprop  48746  ssnn0ssfz  49169  pgrpgt2nabl  49186  eenglngeehlnmlem1  49557