Theorem ssralv 4051

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ss2ralv  4053  intss  4974  iinss1  5013  disjiun  5136  poss  5591  sess2  5646  isores3  7332  isoini2  7336  xpord2indlem  8133  xpord3inddlem  8140  poseq  8144  soseq  8145  smores  8352  smores2  8354  tfrlem5  8380  naddssim  8684  resixp  8927  ac6sfi  9287  iunfi  9340  ixpfi2  9350  marypha1lem  9428  ordtypelem2  9514  ttrclselem2  9721  tcrank  9879  acndom  10046  pwsdompw  10199  ssfin3ds  10325  fin1a2s  10409  hsmexlem4  10424  domtriomlem  10437  zornn0g  10500  fpwwe2lem12  10637  ingru  10810  cshw1  14772  rexanuz  15292  cau3lem  15301  caubnd  15305  limsupgord  15416  limsupval2  15424  rlimres  15502  lo1res  15503  o1of2  15557  o1rlimmul  15563  climsup  15616  fsumiun  15767  lcmfunsnlem1  16574  coprmprod  16598  pcfac  16832  vdwnnlem2  16929  firest  17378  imasaddfnlem  17474  imasvscafn  17483  psss  18533  tsrss  18542  cntz2ss  19199  cntzmhm2  19206  subgpgp  19465  efgsres  19606  telgsumfzs  19857  telgsums  19861  dprdss  19899  acsfn1p  20415  ocv2ss  21226  mretopd  22596  tgcn  22756  tgcnp  22757  subbascn  22758  cnss2  22781  cncnp  22784  sslm  22803  t1ficld  22831  tgcmp  22905  1stcfb  22949  islly2  22988  dislly  23001  comppfsc  23036  ptbasfi  23085  ptcnplem  23125  tx1stc  23154  qtoptop2  23203  fbunfip  23373  flftg  23500  txflf  23510  fclsbas  23525  fclsss1  23526  fclsss2  23527  alexsubb  23550  tmdgsum2  23600  metrest  24033  rescncf  24413  cnllycmp  24472  bndth  24474  fgcfil  24788  ivthlem2  24969  ivthlem3  24970  ovolsslem  25001  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  iunmbl  25070  ioombl1lem4  25078  dyadmax  25115  vitali  25130  mbfimaopnlem  25172  mbflimsup  25183  mbfi1flim  25241  ditgeq3  25367  dvferm  25505  rollelem  25506  dvivthlem1  25525  itgsubstlem  25565  aalioulem2  25846  ulmcaulem  25906  ulmss  25909  xrlimcnp  26473  2sqreunnlem2  26958  pntlem3  27112  pntlemp  27113  pntleml  27114  nosepon  27168  noresle  27200  sssslt1  27297  sssslt2  27298  uspgr2wlkeq  28934  redwlk  28960  wwlksm1edg  29166  wwlksnred  29177  clwlkclwwlklem2  29284  clwwlkinwwlk  29324  clwwlkf  29331  wwlksubclwwlk  29342  occon  30571  xrge0infss  32004  resspos  32167  resstos  32168  gsummptres2  32236  submarchi  32363  prmidl2  32590  sigaclci  33161  measiun  33247  elmbfmvol2  33297  sibfof  33370  ftc2re  33641  bnj1118  34026  subfacp1lem3  34204  iccllysconn  34272  dmopab3rexdif  34427  untint  34712  untangtr  34714  dfon2lem6  34791  dfon2lem8  34793  dfon2lem9  34794  neibastop1  35292  neibastop2lem  35293  neibastop3  35295  finixpnum  36521  ptrecube  36536  poimirlem26  36562  poimirlem27  36563  poimirlem30  36566  heicant  36571  volsupnfl  36581  prdstotbnd  36710  heibor1lem  36725  ispridl2  36954  elrfirn2  41482  rabdiophlem1  41587  dford3lem1  41813  kelac1  41853  ssralv2  43340  ssralv2VD  43675  climinf  44370  limsupvaluz2  44502  supcnvlimsup  44504  iccpartres  46134