Theorem ssralv 3967

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3061   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  ss2ralv  3969  intss  4880  iinss1  4919  disjiun  5040  poss  5470  sess2  5520  isores3  7144  isoini2  7148  smores  8089  smores2  8091  tfrlem5  8116  resixp  8614  ac6sfi  8915  iunfi  8964  ixpfi2  8974  marypha1lem  9049  ordtypelem2  9135  tcrank  9500  acndom  9665  pwsdompw  9818  ssfin3ds  9944  fin1a2s  10028  hsmexlem4  10043  domtriomlem  10056  zornn0g  10119  fpwwe2lem12  10256  ingru  10429  cshw1  14387  rexanuz  14909  cau3lem  14918  caubnd  14922  limsupgord  15033  limsupval2  15041  rlimres  15119  lo1res  15120  o1of2  15174  o1rlimmul  15180  climsup  15233  fsumiun  15385  lcmfunsnlem1  16194  coprmprod  16218  pcfac  16452  vdwnnlem2  16549  firest  16937  imasaddfnlem  17033  imasvscafn  17042  psss  18086  tsrss  18095  cntz2ss  18727  cntzmhm2  18734  subgpgp  18986  efgsres  19128  telgsumfzs  19374  telgsums  19378  dprdss  19416  acsfn1p  19843  ocv2ss  20635  mretopd  21989  tgcn  22149  tgcnp  22150  subbascn  22151  cnss2  22174  cncnp  22177  sslm  22196  t1ficld  22224  tgcmp  22298  1stcfb  22342  islly2  22381  dislly  22394  comppfsc  22429  ptbasfi  22478  ptcnplem  22518  tx1stc  22547  qtoptop2  22596  fbunfip  22766  flftg  22893  txflf  22903  fclsbas  22918  fclsss1  22919  fclsss2  22920  alexsubb  22943  tmdgsum2  22993  metrest  23422  rescncf  23794  cnllycmp  23853  bndth  23855  fgcfil  24168  ivthlem2  24349  ivthlem3  24350  ovolsslem  24381  ovolfiniun  24398  finiunmbl  24441  volfiniun  24444  iunmbl  24450  ioombl1lem4  24458  dyadmax  24495  vitali  24510  mbfimaopnlem  24552  mbflimsup  24563  mbfi1flim  24621  ditgeq3  24747  dvferm  24885  rollelem  24886  dvivthlem1  24905  itgsubstlem  24945  aalioulem2  25226  ulmcaulem  25286  ulmss  25289  xrlimcnp  25851  2sqreunnlem2  26336  pntlem3  26490  pntlemp  26491  pntleml  26492  uspgr2wlkeq  27733  redwlk  27760  wwlksm1edg  27965  wwlksnred  27976  clwlkclwwlklem2  28083  clwwlkinwwlk  28123  clwwlkf  28130  wwlksubclwwlk  28141  occon  29368  xrge0infss  30803  resspos  30963  resstos  30964  gsummptres2  31032  submarchi  31159  prmidl2  31330  sigaclci  31812  measiun  31898  elmbfmvol2  31946  sibfof  32019  ftc2re  32290  bnj1118  32677  subfacp1lem3  32857  iccllysconn  32925  dmopab3rexdif  33080  untint  33366  untangtr  33368  dfon2lem6  33483  dfon2lem8  33485  dfon2lem9  33486  xpord2ind  33531  xpord3ind  33537  poseq  33539  soseq  33540  naddssim  33574  nosepon  33605  noresle  33637  sssslt1  33726  sssslt2  33727  neibastop1  34285  neibastop2lem  34286  neibastop3  34288  finixpnum  35499  ptrecube  35514  poimirlem26  35540  poimirlem27  35541  poimirlem30  35544  heicant  35549  volsupnfl  35559  prdstotbnd  35689  heibor1lem  35704  ispridl2  35933  elrfirn2  40221  rabdiophlem1  40326  dford3lem1  40551  kelac1  40591  ssralv2  41824  ssralv2VD  42159  climinf  42822  limsupvaluz2  42954  supcnvlimsup  42956  iccpartres  44543