Theorem ssrexv 4004

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057  df-ss 3919

This theorem is referenced by:  ss2rexv  4006  ssn0rex  4308  iunss1  4956  onfr  6345  moriotass  7335  frxp  8056  frfi  9169  fisupcl  9354  supgtoreq  9355  brwdom3  9468  unwdomg  9470  frmin  9639  tcrank  9774  hsmexlem2  10315  pwfseqlem3  10548  grur1  10708  suplem1pr  10940  fimaxre2  12064  fiminre2  12067  suprfinzcl  12584  lbzbi  12831  suprzub  12834  uzsupss  12835  zmin  12839  ssnn0fi  13889  elss2prb  14392  scshwfzeqfzo  14730  rexico  15258  rlim3  15402  rlimclim  15450  caurcvgr  15578  alzdvds  16228  bitsfzolem  16342  pclem  16747  0ram2  16930  0ramcl  16932  symgextfo  19332  lsmless1x  19554  lsmless2x  19555  dprdss  19941  ablfac2  20001  subrgdvds  20499  ssrest  23089  locfincf  23444  fbun  23753  fgss  23786  isucn2  24191  metust  24471  psmetutop  24480  lebnumlem3  24887  lebnum  24888  cfil3i  25194  cfilss  25195  fgcfil  25196  iscau4  25204  ivthle  25382  ivthle2  25383  lhop1lem  25943  lhop2  25945  ply1divex  26067  plyss  26129  dgrlem  26159  elqaa  26255  aannenlem2  26262  reeff1olem  26381  rlimcnp  26900  ftalem3  27010  2sqreultblem  27384  2sqreunnlem1  27385  2sqreunnltblem  27387  pntlem3  27545  madess  27819  addsuniflem  27942  mulsuniflem  28086  tgisline  28603  axcontlem2  28941  frgrwopreg1  30293  frgrwopreg2  30294  shless  31334  xlt2addrd  32737  ssnnssfz  32765  xreceu  32897  archirngz  33153  archiabllem1b  33156  1arithidom  33497  dfufd2lem  33509  locfinreflem  33848  crefss  33857  esumpcvgval  34086  sigaclci  34140  eulerpartlemgvv  34384  eulerpartlemgh  34386  signsply0  34559  iccllysconn  35282  satfvsucsuc  35397  fgmin  36403  knoppndvlem18  36562  poimirlem26  37685  poimirlem30  37689  volsupnfl  37704  cover2  37754  filbcmb  37779  istotbnd3  37810  sstotbnd  37814  heibor1lem  37848  isdrngo2  37997  isdrngo3  37998  qsss1  38322  islsati  39032  paddss1  39855  paddss2  39856  hdmap14lem2a  41905  prjspreln0  42641  pellfundre  42913  pellfundge  42914  pellfundglb  42917  hbtlem3  43159  hbtlem5  43160  itgoss  43195  radcnvrat  44346  uzubico  45605  uzubico2  45607  climleltrp  45713  fourierdlem20  46164  smflimlem2  46809  iccelpart  47463  fmtnofac2  47599  grtriprop  47971  ssnn0ssfz  48379  pgrpgt2nabl  48396  eenglngeehlnmlem1  48768