Theorem ssralv 3987

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 3914	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 3107	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ss2ralv  3989  intss  4900  iinss1  4939  disjiun  5061  poss  5505  sess2  5558  isores3  7206  isoini2  7210  smores  8183  smores2  8185  tfrlem5  8211  resixp  8721  ac6sfi  9058  iunfi  9107  ixpfi2  9117  marypha1lem  9192  ordtypelem2  9278  ttrclselem2  9484  tcrank  9642  acndom  9807  pwsdompw  9960  ssfin3ds  10086  fin1a2s  10170  hsmexlem4  10185  domtriomlem  10198  zornn0g  10261  fpwwe2lem12  10398  ingru  10571  cshw1  14535  rexanuz  15057  cau3lem  15066  caubnd  15070  limsupgord  15181  limsupval2  15189  rlimres  15267  lo1res  15268  o1of2  15322  o1rlimmul  15328  climsup  15381  fsumiun  15533  lcmfunsnlem1  16342  coprmprod  16366  pcfac  16600  vdwnnlem2  16697  firest  17143  imasaddfnlem  17239  imasvscafn  17248  psss  18298  tsrss  18307  cntz2ss  18939  cntzmhm2  18946  subgpgp  19202  efgsres  19344  telgsumfzs  19590  telgsums  19594  dprdss  19632  acsfn1p  20067  ocv2ss  20878  mretopd  22243  tgcn  22403  tgcnp  22404  subbascn  22405  cnss2  22428  cncnp  22431  sslm  22450  t1ficld  22478  tgcmp  22552  1stcfb  22596  islly2  22635  dislly  22648  comppfsc  22683  ptbasfi  22732  ptcnplem  22772  tx1stc  22801  qtoptop2  22850  fbunfip  23020  flftg  23147  txflf  23157  fclsbas  23172  fclsss1  23173  fclsss2  23174  alexsubb  23197  tmdgsum2  23247  metrest  23680  rescncf  24060  cnllycmp  24119  bndth  24121  fgcfil  24435  ivthlem2  24616  ivthlem3  24617  ovolsslem  24648  ovolfiniun  24665  finiunmbl  24708  volfiniun  24711  iunmbl  24717  ioombl1lem4  24725  dyadmax  24762  vitali  24777  mbfimaopnlem  24819  mbflimsup  24830  mbfi1flim  24888  ditgeq3  25014  dvferm  25152  rollelem  25153  dvivthlem1  25172  itgsubstlem  25212  aalioulem2  25493  ulmcaulem  25553  ulmss  25556  xrlimcnp  26118  2sqreunnlem2  26603  pntlem3  26757  pntlemp  26758  pntleml  26759  uspgr2wlkeq  28013  redwlk  28040  wwlksm1edg  28246  wwlksnred  28257  clwlkclwwlklem2  28364  clwwlkinwwlk  28404  clwwlkf  28411  wwlksubclwwlk  28422  occon  29649  xrge0infss  31083  resspos  31244  resstos  31245  gsummptres2  31313  submarchi  31440  prmidl2  31616  sigaclci  32100  measiun  32186  elmbfmvol2  32234  sibfof  32307  ftc2re  32578  bnj1118  32964  subfacp1lem3  33144  iccllysconn  33212  dmopab3rexdif  33367  untint  33653  untangtr  33655  dfon2lem6  33764  dfon2lem8  33766  dfon2lem9  33767  xpord2ind  33794  xpord3ind  33800  poseq  33802  soseq  33803  naddssim  33837  nosepon  33868  noresle  33900  sssslt1  33989  sssslt2  33990  neibastop1  34548  neibastop2lem  34549  neibastop3  34551  finixpnum  35762  ptrecube  35777  poimirlem26  35803  poimirlem27  35804  poimirlem30  35807  heicant  35812  volsupnfl  35822  prdstotbnd  35952  heibor1lem  35967  ispridl2  36196  elrfirn2  40518  rabdiophlem1  40623  dford3lem1  40848  kelac1  40888  ssralv2  42151  ssralv2VD  42486  climinf  43147  limsupvaluz2  43279  supcnvlimsup  43281  iccpartres  44870