Theorem ssrexv 4052

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537  ∃wex 1778   ∈ wcel 2107  ∃wrex 3069   ⊆ wss 3950

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3070  df-ss 3967

This theorem is referenced by:  ss2rexv  4054  ssn0rex  4357  iunss1  5005  onfr  6422  moriotass  7421  frxp  8152  frfi  9322  fisupcl  9510  supgtoreq  9511  brwdom3  9623  unwdomg  9625  frmin  9790  tcrank  9925  hsmexlem2  10468  pwfseqlem3  10701  grur1  10861  suplem1pr  11093  fimaxre2  12214  fiminre2  12217  suprfinzcl  12734  lbzbi  12979  suprzub  12982  uzsupss  12983  zmin  12987  ssnn0fi  14027  elss2prb  14528  scshwfzeqfzo  14866  rexico  15393  rlim3  15535  rlimclim  15583  caurcvgr  15711  alzdvds  16358  bitsfzolem  16472  pclem  16877  0ram2  17060  0ramcl  17062  symgextfo  19441  lsmless1x  19663  lsmless2x  19664  dprdss  20050  ablfac2  20110  subrgdvds  20587  ssrest  23185  locfincf  23540  fbun  23849  fgss  23882  isucn2  24289  metust  24572  psmetutop  24581  lebnumlem3  24996  lebnum  24997  cfil3i  25304  cfilss  25305  fgcfil  25306  iscau4  25314  ivthle  25492  ivthle2  25493  lhop1lem  26053  lhop2  26055  ply1divex  26177  plyss  26239  dgrlem  26269  elqaa  26365  aannenlem2  26372  reeff1olem  26491  rlimcnp  27009  ftalem3  27119  2sqreultblem  27493  2sqreunnlem1  27494  2sqreunnltblem  27496  pntlem3  27654  madess  27916  addsuniflem  28035  mulsuniflem  28176  tgisline  28636  axcontlem2  28981  frgrwopreg1  30338  frgrwopreg2  30339  shless  31379  xlt2addrd  32763  ssnnssfz  32790  xreceu  32905  archirngz  33197  archiabllem1b  33200  1arithidom  33566  dfufd2lem  33578  locfinreflem  33840  crefss  33849  esumpcvgval  34080  sigaclci  34134  eulerpartlemgvv  34379  eulerpartlemgh  34381  signsply0  34567  iccllysconn  35256  satfvsucsuc  35371  fgmin  36372  knoppndvlem18  36531  poimirlem26  37654  poimirlem30  37658  volsupnfl  37673  cover2  37723  filbcmb  37748  istotbnd3  37779  sstotbnd  37783  heibor1lem  37817  isdrngo2  37966  isdrngo3  37967  qsss1  38291  islsati  38996  paddss1  39820  paddss2  39821  hdmap14lem2a  41870  prjspreln0  42624  pellfundre  42897  pellfundge  42898  pellfundglb  42901  hbtlem3  43144  hbtlem5  43145  itgoss  43180  radcnvrat  44338  uzubico  45586  uzubico2  45588  climleltrp  45696  fourierdlem20  46147  smflimlem2  46792  iccelpart  47425  fmtnofac2  47561  grtriprop  47913  ssnn0ssfz  48270  pgrpgt2nabl  48287  eenglngeehlnmlem1  48663