Theorem ssralv 3960

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

Syntax hints:   → wi 4   ∈ wcel 2083  ∀wral 3107   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-in 3872  df-ss 3880

This theorem is referenced by:  ss2ralv  3962  intss  4809  iinss1  4845  disjiun  4956  poss  5371  sess2  5419  isores3  6958  isoini2  6962  smores  7848  smores2  7850  tfrlem5  7875  resixp  8352  ac6sfi  8615  iunfi  8665  ixpfi2  8675  marypha1lem  8750  ordtypelem2  8836  tcrank  9166  acndom  9330  pwsdompw  9479  ssfin3ds  9605  fin1a2s  9689  hsmexlem4  9704  domtriomlem  9717  zornn0g  9780  fpwwe2lem13  9917  ingru  10090  cshw1  14024  rexanuz  14543  cau3lem  14552  caubnd  14556  limsupgord  14667  limsupval2  14675  rlimres  14753  lo1res  14754  o1of2  14807  o1rlimmul  14813  climsup  14864  fsumiun  15013  lcmfunsnlem1  15814  coprmprod  15838  pcfac  16068  vdwnnlem2  16165  firest  16539  imasaddfnlem  16634  imasvscafn  16643  psss  17657  tsrss  17666  cntz2ss  18208  cntzmhm2  18215  subgpgp  18456  efgsres  18595  telgsumfzs  18830  telgsums  18834  dprdss  18872  acsfn1p  19272  ocv2ss  20503  mretopd  21388  tgcn  21548  tgcnp  21549  subbascn  21550  cnss2  21573  cncnp  21576  sslm  21595  t1ficld  21623  tgcmp  21697  1stcfb  21741  islly2  21780  dislly  21793  comppfsc  21828  ptbasfi  21877  ptcnplem  21917  tx1stc  21946  qtoptop2  21995  fbunfip  22165  flftg  22292  txflf  22302  fclsbas  22317  fclsss1  22318  fclsss2  22319  alexsubb  22342  tmdgsum2  22392  metrest  22821  rescncf  23192  cnllycmp  23247  bndth  23249  fgcfil  23561  ivthlem2  23740  ivthlem3  23741  ovolsslem  23772  ovolfiniun  23789  finiunmbl  23832  volfiniun  23835  iunmbl  23841  ioombl1lem4  23849  dyadmax  23886  vitali  23901  mbfimaopnlem  23943  mbflimsup  23954  mbfi1flim  24011  ditgeq3  24135  dvferm  24272  rollelem  24273  dvivthlem1  24292  itgsubstlem  24332  aalioulem2  24609  ulmcaulem  24669  ulmss  24672  xrlimcnp  25232  2sqreunnlem2  25717  pntlem3  25871  pntlemp  25872  pntleml  25873  uspgr2wlkeq  27114  redwlk  27140  wwlksm1edg  27345  wwlksnred  27356  clwlkclwwlklem2  27464  clwwlkinwwlk  27504  clwwlkf  27512  wwlksubclwwlk  27523  occon  28751  xrge0infss  30168  resspos  30316  resstos  30317  submarchi  30449  sigaclci  31004  measiun  31090  elmbfmvol2  31138  sibfof  31211  ftc2re  31482  bnj1118  31866  subfacp1lem3  32039  iccllysconn  32107  dmopab3rexdif  32262  untint  32548  untangtr  32550  dfon2lem6  32643  dfon2lem8  32645  dfon2lem9  32646  poseq  32706  soseq  32707  nosepon  32783  noresle  32811  sssslt1  32871  sssslt2  32872  neibastop1  33318  neibastop2lem  33319  neibastop3  33321  finixpnum  34429  ptrecube  34444  poimirlem26  34470  poimirlem27  34471  poimirlem30  34474  heicant  34479  volsupnfl  34489  prdstotbnd  34625  heibor1lem  34640  ispridl2  34869  elrfirn2  38799  rabdiophlem1  38904  dford3lem1  39129  kelac1  39169  ssralv2  40425  ssralv2VD  40760  climinf  41450  limsupvaluz2  41582  supcnvlimsup  41584  iccpartres  43082