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  34798  eulerpartlemgh  34800  signsply0  34970  iccllysconn  35763  satfvsucsuc  35878  fgmin  36922  knoppndvlem18  37159  poimirlem26  38338  poimirlem30  38342  volsupnfl  38357  cover2  38407  filbcmb  38432  istotbnd3  38463  sstotbnd  38467  heibor1lem  38501  isdrngo2  38650  isdrngo3  38651  qsss1  38985  islsati  39809  paddss1  40632  paddss2  40633  hdmap14lem2a  42682  prjspreln0  43382  pellfundre  43649  pellfundge  43650  pellfundglb  43653  hbtlem3  43895  hbtlem5  43896  itgoss  43931  radcnvrat  45065  uzubico  46323  uzubico2  46325  climleltrp  46431  fourierdlem20  46882  smflimlem2  47527  nndivides2  48162  iccelpart  48223  fmtnofac2  48362  grtriprop  48747  ssnn0ssfz  49170  pgrpgt2nabl  49187  eenglngeehlnmlem1  49558