Theorem ssrexv 3978

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 3896	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1864	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3087	. . 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 1567  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086   ⊆ wss 3895

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087  df-ss 3896

This theorem is used by:  ss2rexv  3980  ssn0rex  4305  iunss1  4965  onfr  6402  moriotass  7409  frxp  8140  frfi  9279  fisupcl  9465  supgtoreq  9466  brwdom3  9579  unwdomg  9581  frmin  9756  tcrank  9904  hsmexlem2  10508  pwfseqlem3  10748  grur1  10908  suplem1pr  11140  fimaxre2  12265  fiminre2  12268  suprfinzcl  12816  lbzbi  13066  suprzub  13069  uzsupss  13070  zmin  13074  ssnn0fi  14131  elss2prb  14636  scshwfzeqfzo  14981  rexico  15526  rlim3  15670  rlimclim  15718  caurcvgr  15846  alzdvds  16495  bitsfzolem  16609  pclem  17021  0ram2  17204  0ramcl  17206  symgextfo  19641  lsmless1x  19863  lsmless2x  19864  dprdss  20250  ablfac2  20310  subrgdvds  20843  isdrng3lem2  21011  isdrng5  21013  ssrest  23499  locfincf  23855  fbun  24164  fgss  24197  isucn2  24602  metust  24882  psmetutop  24891  lebnumlem3  25289  lebnum  25290  cfil3i  25595  cfilss  25596  fgcfil  25597  iscau4  25605  ivthle  25782  ivthle2  25783  lhop1lem  26338  lhop2  26340  ply1divex  26460  plyss  26522  dgrlem  26553  elqaa  26650  aannenlem2  26661  reeff1olem  26778  rlimcnp  27298  ftalem3  27407  2sqreultblem  27780  2sqreunnlem1  27781  2sqreunnltblem  27783  pntlem3  27941  madess  28257  addsuniflem  28392  mulsuniflem  28540  tgisline  29100  axcontlem2  29548  frgrwopreg1  30924  frgrwopreg2  30925  shless  31966  xlt2addrd  33397  ssnnssfz  33425  xreceu  33534  archirngz  33796  archiabllem1b  33799  1arithidom  34115  dfufd2lem  34127  locfinreflem  34518  crefss  34527  esumpcvgval  34756  sigaclci  34810  eulerpartlemgvv  35054  eulerpartlemgh  35056  signsply0  35226  prconf1acwevd  35967  iccllysconn  36101  satfvsucsuc  36216  fgmin  37250  knoppndvlem18  37487  poimirlem26  38657  poimirlem30  38661  volsupnfl  38676  dfprop2  38739  cover2  38742  filbcmb  38767  istotbnd3  38798  sstotbnd  38802  heibor1lem  38836  isdrngo2  38985  isdrngo3  38986  qsss1  39320  islsati  40144  paddss1  40967  paddss2  40968  hdmap14lem2a  43017  prjspreln0  43730  pellfundre  43981  pellfundge  43982  pellfundglb  43985  hbtlem3  44222  hbtlem5  44223  itgoss  44258  radcnvrat  45391  uzubico  46671  uzubico2  46673  climleltrp  46779  fourierdlem20  47230  smflimlem2  47875  nndivides2  48547  iccelpart  48608  fmtnofac2  48747  grtriprop  49132  ssnn0ssfz  49554  pgrpgt2nabl  49571  eenglngeehlnmlem1  49943