Theorem ssrexv 3991

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 628	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1839	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3065	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3065	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))
7	1, 6	sylbi 218	1 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065  df-ss 3907

This theorem is referenced by:  ss2rexv  3993  ssn0rex  4293  iunss1  4943  onfr  6356  moriotass  7352  frxp  8073  frfi  9192  fisupcl  9380  supgtoreq  9381  brwdom3  9494  unwdomg  9496  frmin  9671  tcrank  9806  hsmexlem2  10347  pwfseqlem3  10581  grur1  10741  suplem1pr  10973  fimaxre2  12099  fiminre2  12102  suprfinzcl  12641  lbzbi  12884  suprzub  12887  uzsupss  12888  zmin  12892  ssnn0fi  13945  elss2prb  14448  scshwfzeqfzo  14786  rexico  15314  rlim3  15458  rlimclim  15506  caurcvgr  15634  alzdvds  16287  bitsfzolem  16401  pclem  16807  0ram2  16990  0ramcl  16992  symgextfo  19395  lsmless1x  19617  lsmless2x  19618  dprdss  20004  ablfac2  20064  subrgdvds  20565  ssrest  23166  locfincf  23521  fbun  23830  fgss  23863  isucn2  24268  metust  24548  psmetutop  24557  lebnumlem3  24955  lebnum  24956  cfil3i  25261  cfilss  25262  fgcfil  25263  iscau4  25271  ivthle  25448  ivthle2  25449  lhop1lem  26005  lhop2  26007  ply1divex  26127  plyss  26189  dgrlem  26219  elqaa  26313  aannenlem2  26320  reeff1olem  26436  rlimcnp  26954  ftalem3  27063  2sqreultblem  27436  2sqreunnlem1  27437  2sqreunnltblem  27439  pntlem3  27597  madess  27883  addsuniflem  28018  mulsuniflem  28166  tgisline  28720  axcontlem2  29059  frgrwopreg1  30413  frgrwopreg2  30414  shless  31455  xlt2addrd  32858  ssnnssfz  32886  xreceu  33007  archirngz  33277  archiabllem1b  33280  1arithidom  33627  dfufd2lem  33639  locfinreflem  34031  crefss  34040  esumpcvgval  34269  sigaclci  34323  eulerpartlemgvv  34567  eulerpartlemgh  34569  signsply0  34742  iccllysconn  35485  satfvsucsuc  35600  fgmin  36605  knoppndvlem18  36842  poimirlem26  38020  poimirlem30  38024  volsupnfl  38039  cover2  38089  filbcmb  38114  istotbnd3  38145  sstotbnd  38149  heibor1lem  38183  isdrngo2  38332  isdrngo3  38333  qsss1  38669  islsati  39493  paddss1  40316  paddss2  40317  hdmap14lem2a  42366  prjspreln0  43066  pellfundre  43333  pellfundge  43334  pellfundglb  43337  hbtlem3  43579  hbtlem5  43580  itgoss  43615  radcnvrat  44765  uzubico  46018  uzubico2  46020  climleltrp  46126  fourierdlem20  46577  smflimlem2  47222  nndivides2  47854  iccelpart  47915  fmtnofac2  48054  grtriprop  48439  ssnn0ssfz  48847  pgrpgt2nabl  48864  eenglngeehlnmlem1  49235