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  27296  sssslt2  27297  uspgr2wlkeq  28903  redwlk  28929  wwlksm1edg  29135  wwlksnred  29146  clwlkclwwlklem2  29253  clwwlkinwwlk  29293  clwwlkf  29300  wwlksubclwwlk  29311  occon  30540  xrge0infss  31973  resspos  32136  resstos  32137  gsummptres2  32205  submarchi  32332  prmidl2  32559  sigaclci  33130  measiun  33216  elmbfmvol2  33266  sibfof  33339  ftc2re  33610  bnj1118  33995  subfacp1lem3  34173  iccllysconn  34241  dmopab3rexdif  34396  untint  34681  untangtr  34683  dfon2lem6  34760  dfon2lem8  34762  dfon2lem9  34763  neibastop1  35244  neibastop2lem  35245  neibastop3  35247  finixpnum  36473  ptrecube  36488  poimirlem26  36514  poimirlem27  36515  poimirlem30  36518  heicant  36523  volsupnfl  36533  prdstotbnd  36662  heibor1lem  36677  ispridl2  36906  elrfirn2  41434  rabdiophlem1  41539  dford3lem1  41765  kelac1  41805  ssralv2  43292  ssralv2VD  43627  climinf  44322  limsupvaluz2  44454  supcnvlimsup  44456  iccpartres  46086