Theorem ssralv 3629

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3562	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 80	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 2944	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-in 3547  df-ss 3554

This theorem is referenced by:  intss  4433  iinss1  4469  disjiun  4573  poss  4961  sess2  5007  isores3  6485  isoini2  6489  smores  7336  smores2  7338  tfrlem5  7363  resixp  7829  ac6sfi  8089  iunfi  8137  ixpfi2  8147  dffi3  8220  marypha1lem  8222  ordtypelem2  8307  tcrank  8630  acndom  8757  pwsdompw  8909  ssfin3ds  9035  fin1a2s  9119  hsmexlem4  9134  domtriomlem  9147  zornn0g  9210  fpwwe2lem13  9343  ingru  9516  cshw1  13419  rexanuz  13933  cau3lem  13942  caubnd  13946  limsupgord  14051  limsupval2  14059  rlimres  14137  lo1res  14138  o1of2  14191  o1rlimmul  14197  isercolllem1  14243  climsup  14248  fsumiun  14394  lcmfunsnlem1  15188  coprmprod  15213  pcfac  15441  vdwnnlem2  15538  firest  15916  imasaddfnlem  16011  imasvscafn  16020  psss  17037  tsrss  17046  cntz2ss  17588  cntzmhm2  17595  subgpgp  17835  efgsres  17974  telgsumfzs  18209  telgsums  18213  dprdss  18251  ocv2ss  19836  mretopd  20706  tgcn  20866  tgcnp  20867  subbascn  20868  cnss2  20891  cncnp  20894  sslm  20913  t1ficld  20941  tgcmp  21014  1stcfb  21058  islly2  21097  dislly  21110  comppfsc  21145  ptbasfi  21194  ptcnplem  21234  tx1stc  21263  qtoptop2  21312  fbunfip  21483  flftg  21610  txflf  21620  fclsbas  21635  fclsss1  21636  fclsss2  21637  alexsubb  21660  tmdgsum2  21710  metrest  22139  rescncf  22508  cnllycmp  22563  bndth  22565  fgcfil  22877  cfilres  22902  ivthlem2  23028  ivthlem3  23029  ovolsslem  23059  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  iunmbl  23128  ioombl1lem4  23136  dyadmax  23172  vitali  23188  mbfimaopnlem  23228  mbflimsup  23239  mbfi1flim  23296  ditgeq3  23420  dvferm  23555  rollelem  23556  dvivthlem1  23575  itgsubstlem  23615  aalioulem2  23892  ulmcaulem  23952  ulmss  23955  xrlimcnp  24495  lgsdchr  24880  pntlem3  25098  pntlemp  25099  pntleml  25100  nbgraf1olem1  25970  redwlk  26136  usg2wlkeq  26236  wwlknred  26251  wwlkm1edg  26263  clwlkisclwwlklem1  26315  clwwlkf  26322  wwlksubclwwlk  26332  extwwlkfablem2  26605  occon  27530  xrge0infss  28915  resspos  28990  resstos  28991  submarchi  29071  sigaclci  29522  measiun  29608  elmbfmvol2  29656  sibfof  29729  bnj1118  30306  subfacp1lem3  30418  iccllyscon  30486  untint  30843  untangtr  30845  dfon2lem6  30937  dfon2lem8  30939  dfon2lem9  30940  poseq  30994  soseq  30995  nosepon  31066  neibastop1  31524  neibastop2lem  31525  neibastop3  31527  finixpnum  32564  ptrecube  32579  poimirlem26  32605  poimirlem27  32606  poimirlem30  32609  heicant  32614  volsupnfl  32624  prdstotbnd  32763  heibor1lem  32778  ispridl2  33007  elrfirn2  36277  rabdiophlem1  36383  dford3lem1  36611  kelac1  36651  acsfn1p  36788  ssralv2  37758  ssralv2VD  38124  climinf  38673  iccpartres  39956  uspgr2wlkeq  40854  red1wlk  40881  wwlksm1edg  41078  wwlksnred  41098  clwlkclwwlklem2  41209  clwwlksf  41222  wwlksubclwwlks  41232  av-extwwlkfablem2  41510