Theorem ssralv 4015

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3060   ⊆ wss 3913

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ss2ralv  4017  intss  4935  iinss1  4974  disjiun  5097  poss  5552  sess2  5607  isores3  7285  isoini2  7289  xpord2indlem  8084  xpord3inddlem  8091  poseq  8095  soseq  8096  smores  8303  smores2  8305  tfrlem5  8331  naddssim  8636  resixp  8878  ac6sfi  9238  iunfi  9291  ixpfi2  9301  marypha1lem  9378  ordtypelem2  9464  ttrclselem2  9671  tcrank  9829  acndom  9996  pwsdompw  10149  ssfin3ds  10275  fin1a2s  10359  hsmexlem4  10374  domtriomlem  10387  zornn0g  10450  fpwwe2lem12  10587  ingru  10760  cshw1  14722  rexanuz  15242  cau3lem  15251  caubnd  15255  limsupgord  15366  limsupval2  15374  rlimres  15452  lo1res  15453  o1of2  15507  o1rlimmul  15513  climsup  15566  fsumiun  15717  lcmfunsnlem1  16524  coprmprod  16548  pcfac  16782  vdwnnlem2  16879  firest  17328  imasaddfnlem  17424  imasvscafn  17433  psss  18483  tsrss  18492  cntz2ss  19127  cntzmhm2  19134  subgpgp  19393  efgsres  19534  telgsumfzs  19780  telgsums  19784  dprdss  19822  acsfn1p  20322  ocv2ss  21114  mretopd  22480  tgcn  22640  tgcnp  22641  subbascn  22642  cnss2  22665  cncnp  22668  sslm  22687  t1ficld  22715  tgcmp  22789  1stcfb  22833  islly2  22872  dislly  22885  comppfsc  22920  ptbasfi  22969  ptcnplem  23009  tx1stc  23038  qtoptop2  23087  fbunfip  23257  flftg  23384  txflf  23394  fclsbas  23409  fclsss1  23410  fclsss2  23411  alexsubb  23434  tmdgsum2  23484  metrest  23917  rescncf  24297  cnllycmp  24356  bndth  24358  fgcfil  24672  ivthlem2  24853  ivthlem3  24854  ovolsslem  24885  ovolfiniun  24902  finiunmbl  24945  volfiniun  24948  iunmbl  24954  ioombl1lem4  24962  dyadmax  24999  vitali  25014  mbfimaopnlem  25056  mbflimsup  25067  mbfi1flim  25125  ditgeq3  25251  dvferm  25389  rollelem  25390  dvivthlem1  25409  itgsubstlem  25449  aalioulem2  25730  ulmcaulem  25790  ulmss  25793  xrlimcnp  26355  2sqreunnlem2  26840  pntlem3  26994  pntlemp  26995  pntleml  26996  nosepon  27050  noresle  27082  sssslt1  27177  sssslt2  27178  uspgr2wlkeq  28657  redwlk  28683  wwlksm1edg  28889  wwlksnred  28900  clwlkclwwlklem2  29007  clwwlkinwwlk  29047  clwwlkf  29054  wwlksubclwwlk  29065  occon  30292  xrge0infss  31733  resspos  31896  resstos  31897  gsummptres2  31965  submarchi  32092  prmidl2  32289  sigaclci  32820  measiun  32906  elmbfmvol2  32956  sibfof  33029  ftc2re  33300  bnj1118  33685  subfacp1lem3  33863  iccllysconn  33931  dmopab3rexdif  34086  untint  34370  untangtr  34372  dfon2lem6  34449  dfon2lem8  34451  dfon2lem9  34452  neibastop1  34907  neibastop2lem  34908  neibastop3  34910  finixpnum  36136  ptrecube  36151  poimirlem26  36177  poimirlem27  36178  poimirlem30  36181  heicant  36186  volsupnfl  36196  prdstotbnd  36326  heibor1lem  36341  ispridl2  36570  elrfirn2  41077  rabdiophlem1  41182  dford3lem1  41408  kelac1  41448  ssralv2  42935  ssralv2VD  43270  climinf  43967  limsupvaluz2  44099  supcnvlimsup  44101  iccpartres  45730