Theorem ssrexv 3983

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 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		pm3.45 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4		df-rex 3091	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rex 3091	. . 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 2147  ∃wrex 3090   ⊆ wss 3900

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 3091  df-ss 3901

This theorem is used by:  ss2rexv  3985  ssn0rex  4309  iunss1  4969  onfr  6420  moriotass  7432  frxp  8165  frfi  9304  fisupcl  9489  supgtoreq  9490  brwdom3  9603  unwdomg  9605  frmin  9780  tcrank  9928  hsmexlem2  10532  pwfseqlem3  10772  grur1  10932  suplem1pr  11164  fimaxre2  12289  fiminre2  12292  suprfinzcl  12840  lbzbi  13090  suprzub  13093  uzsupss  13094  zmin  13098  ssnn0fi  14155  elss2prb  14660  scshwfzeqfzo  15005  rexico  15550  rlim3  15694  rlimclim  15742  caurcvgr  15870  alzdvds  16519  bitsfzolem  16633  pclem  17045  0ram2  17228  0ramcl  17230  symgextfo  19666  lsmless1x  19888  lsmless2x  19889  dprdss  20275  ablfac2  20335  subrgdvds  20868  isdrng3lem2  21036  isdrng5  21038  ssrest  23524  locfincf  23880  fbun  24189  fgss  24222  isucn2  24627  metust  24907  psmetutop  24916  lebnumlem3  25314  lebnum  25315  cfil3i  25620  cfilss  25621  fgcfil  25622  iscau4  25630  ivthle  25807  ivthle2  25808  lhop1lem  26363  lhop2  26365  ply1divex  26485  plyss  26547  dgrlem  26578  elqaa  26675  aannenlem2  26686  reeff1olem  26803  rlimcnp  27323  ftalem3  27432  2sqreultblem  27805  2sqreunnlem1  27806  2sqreunnltblem  27808  pntlem3  27966  madess  28282  addsuniflem  28417  mulsuniflem  28565  tgisline  29125  axcontlem2  29573  frgrwopreg1  30949  frgrwopreg2  30950  shless  31991  xlt2addrd  33421  ssnnssfz  33449  xreceu  33558  archirngz  33820  archiabllem1b  33823  1arithidom  34139  dfufd2lem  34151  locfinreflem  34542  crefss  34551  esumpcvgval  34780  sigaclci  34834  eulerpartlemgvv  35078  eulerpartlemgh  35080  signsply0  35250  prconf1acwevd  36048  iccllysconn  36182  satfvsucsuc  36297  fgmin  37336  knoppndvlem18  37573  poimirlem26  38756  poimirlem30  38760  volsupnfl  38775  dfprop2  38838  cover2  38841  filbcmb  38866  istotbnd3  38897  sstotbnd  38901  heibor1lem  38935  isdrngo2  39084  isdrngo3  39085  qsss1  39419  islsati  40243  paddss1  41066  paddss2  41067  hdmap14lem2a  43116  prjspreln0  43830  pellfundre  44081  pellfundge  44082  pellfundglb  44085  hbtlem3  44321  hbtlem5  44322  itgoss  44357  radcnvrat  45490  uzubico  46783  uzubico2  46785  climleltrp  46891  fourierdlem20  47342  smflimlem2  47987  nndivides2  48659  iccelpart  48720  fmtnofac2  48859  grtriprop  49244  ssnn0ssfz  49666  pgrpgt2nabl  49683  eenglngeehlnmlem1  50055