Theorem ssralv 3815

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

Syntax hints:   → wi 4   ∈ wcel 2145  ∀wral 3061   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ral 3066  df-in 3730  df-ss 3737

This theorem is referenced by:  intss  4632  iinss1  4667  disjiun  4774  poss  5172  sess2  5218  isores3  6728  isoini2  6732  smores  7602  smores2  7604  tfrlem5  7629  resixp  8097  ac6sfi  8360  iunfi  8410  ixpfi2  8420  dffi3  8493  marypha1lem  8495  ordtypelem2  8580  tcrank  8911  acndom  9074  pwsdompw  9228  ssfin3ds  9354  fin1a2s  9438  hsmexlem4  9453  domtriomlem  9466  zornn0g  9529  fpwwe2lem13  9666  ingru  9839  cshw1  13777  rexanuz  14293  cau3lem  14302  caubnd  14306  limsupgord  14411  limsupval2  14419  rlimres  14497  lo1res  14498  o1of2  14551  o1rlimmul  14557  isercolllem1  14603  climsup  14608  fsumiun  14760  lcmfunsnlem1  15558  coprmprod  15582  pcfac  15810  vdwnnlem2  15907  firest  16301  imasaddfnlem  16396  imasvscafn  16405  psss  17422  tsrss  17431  cntz2ss  17972  cntzmhm2  17979  subgpgp  18219  efgsres  18358  telgsumfzs  18594  telgsums  18598  dprdss  18636  ocv2ss  20234  mretopd  21117  tgcn  21277  tgcnp  21278  subbascn  21279  cnss2  21302  cncnp  21305  sslm  21324  t1ficld  21352  tgcmp  21425  1stcfb  21469  islly2  21508  dislly  21521  comppfsc  21556  ptbasfi  21605  ptcnplem  21645  tx1stc  21674  qtoptop2  21723  fbunfip  21893  flftg  22020  txflf  22030  fclsbas  22045  fclsss1  22046  fclsss2  22047  alexsubb  22070  tmdgsum2  22120  metrest  22549  rescncf  22920  cnllycmp  22975  bndth  22977  fgcfil  23288  cfilres  23313  ivthlem2  23440  ivthlem3  23441  ovolsslem  23472  ovolfiniun  23489  finiunmbl  23532  volfiniun  23535  iunmbl  23541  ioombl1lem4  23549  dyadmax  23586  vitali  23601  mbfimaopnlem  23642  mbflimsup  23653  mbfi1flim  23710  ditgeq3  23834  dvferm  23971  rollelem  23972  dvivthlem1  23991  itgsubstlem  24031  aalioulem2  24308  ulmcaulem  24368  ulmss  24371  xrlimcnp  24916  lgsdchr  25301  pntlem3  25519  pntlemp  25520  pntleml  25521  uspgr2wlkeq  26777  redwlk  26804  wwlksm1edg  27015  wwlksnred  27036  clwlkclwwlklem2  27150  clwwlkinwwlk  27196  clwwlkf  27203  wwlksubclwwlk  27216  occon  28486  xrge0infss  29865  resspos  29999  resstos  30000  submarchi  30080  sigaclci  30535  measiun  30621  elmbfmvol2  30669  sibfof  30742  ftc2re  31016  bnj1118  31390  subfacp1lem3  31502  iccllysconn  31570  untint  31927  untangtr  31929  dfon2lem6  32029  dfon2lem8  32031  dfon2lem9  32032  poseq  32090  soseq  32091  nosepon  32155  noresle  32183  sssslt1  32243  sssslt2  32244  neibastop1  32691  neibastop2lem  32692  neibastop3  32694  finixpnum  33727  ptrecube  33742  poimirlem26  33768  poimirlem27  33769  poimirlem30  33772  heicant  33777  volsupnfl  33787  prdstotbnd  33925  heibor1lem  33940  ispridl2  34169  elrfirn2  37785  rabdiophlem1  37891  dford3lem1  38119  kelac1  38159  acsfn1p  38295  ssralv2  39262  ssralv2VD  39624  climinf  40356  limsupvaluz2  40488  supcnvlimsup  40490  iccpartres  41882