Theorem ssralv 4008

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3062   ⊆ wss 3908

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-v 3445  df-in 3915  df-ss 3925

This theorem is referenced by:  ss2ralv  4010  intss  4928  iinss1  4967  disjiun  5090  poss  5545  sess2  5600  isores3  7276  isoini2  7280  xpord2indlem  8071  xpord3inddlem  8078  poseq  8082  soseq  8083  smores  8290  smores2  8292  tfrlem5  8318  resixp  8829  ac6sfi  9189  iunfi  9242  ixpfi2  9252  marypha1lem  9327  ordtypelem2  9413  ttrclselem2  9620  tcrank  9778  acndom  9945  pwsdompw  10098  ssfin3ds  10224  fin1a2s  10308  hsmexlem4  10323  domtriomlem  10336  zornn0g  10399  fpwwe2lem12  10536  ingru  10709  cshw1  14664  rexanuz  15184  cau3lem  15193  caubnd  15197  limsupgord  15308  limsupval2  15316  rlimres  15394  lo1res  15395  o1of2  15449  o1rlimmul  15455  climsup  15508  fsumiun  15660  lcmfunsnlem1  16467  coprmprod  16491  pcfac  16725  vdwnnlem2  16822  firest  17268  imasaddfnlem  17364  imasvscafn  17373  psss  18423  tsrss  18432  cntz2ss  19066  cntzmhm2  19073  subgpgp  19332  efgsres  19473  telgsumfzs  19719  telgsums  19723  dprdss  19761  acsfn1p  20213  ocv2ss  21024  mretopd  22389  tgcn  22549  tgcnp  22550  subbascn  22551  cnss2  22574  cncnp  22577  sslm  22596  t1ficld  22624  tgcmp  22698  1stcfb  22742  islly2  22781  dislly  22794  comppfsc  22829  ptbasfi  22878  ptcnplem  22918  tx1stc  22947  qtoptop2  22996  fbunfip  23166  flftg  23293  txflf  23303  fclsbas  23318  fclsss1  23319  fclsss2  23320  alexsubb  23343  tmdgsum2  23393  metrest  23826  rescncf  24206  cnllycmp  24265  bndth  24267  fgcfil  24581  ivthlem2  24762  ivthlem3  24763  ovolsslem  24794  ovolfiniun  24811  finiunmbl  24854  volfiniun  24857  iunmbl  24863  ioombl1lem4  24871  dyadmax  24908  vitali  24923  mbfimaopnlem  24965  mbflimsup  24976  mbfi1flim  25034  ditgeq3  25160  dvferm  25298  rollelem  25299  dvivthlem1  25318  itgsubstlem  25358  aalioulem2  25639  ulmcaulem  25699  ulmss  25702  xrlimcnp  26264  2sqreunnlem2  26749  pntlem3  26903  pntlemp  26904  pntleml  26905  nosepon  26959  noresle  26991  sssslt1  27080  sssslt2  27081  uspgr2wlkeq  28439  redwlk  28465  wwlksm1edg  28671  wwlksnred  28682  clwlkclwwlklem2  28789  clwwlkinwwlk  28829  clwwlkf  28836  wwlksubclwwlk  28847  occon  30074  xrge0infss  31507  resspos  31668  resstos  31669  gsummptres2  31737  submarchi  31864  prmidl2  32051  sigaclci  32559  measiun  32645  elmbfmvol2  32695  sibfof  32768  ftc2re  33039  bnj1118  33424  subfacp1lem3  33604  iccllysconn  33672  dmopab3rexdif  33827  untint  34111  untangtr  34113  dfon2lem6  34195  dfon2lem8  34197  dfon2lem9  34198  naddssim  34256  neibastop1  34763  neibastop2lem  34764  neibastop3  34766  finixpnum  35995  ptrecube  36010  poimirlem26  36036  poimirlem27  36037  poimirlem30  36040  heicant  36045  volsupnfl  36055  prdstotbnd  36185  heibor1lem  36200  ispridl2  36429  elrfirn2  40922  rabdiophlem1  41027  dford3lem1  41253  kelac1  41293  ssralv2  42718  ssralv2VD  43053  climinf  43742  limsupvaluz2  43874  supcnvlimsup  43876  iccpartres  45505