Theorem 2ralbidv 2901

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

Ref	Expression
2ralbidv.1

Assertion

Ref	Expression
2ralbidv

Distinct variable groups:   ,   ,

Proof of Theorem 2ralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3
2	1	ralbidv 2896	. 2
3	2	ralbidv 2896	1

Syntax hints:  ->wi 4  <->wb 184  A.wral 2807

This theorem is referenced by:  cbvral3v  3094  ralxpxfr2d  3224  poeq1  4808  soeq1  4824  isoeq1  6215  isoeq2  6216  isoeq3  6217  fnmpt2ovd  6878  smoeq  7040  xpf1o  7699  nqereu  9328  dedekind  9765  dedekindle  9766  seqcaopr2  12143  wrd2ind  12703  addcn2  13416  mulcn2  13418  mreexexd  15045  catlid  15080  catrid  15081  isfunc  15233  funcres2b  15266  isfull  15279  isfth  15283  fullres2c  15308  isnat  15316  evlfcl  15491  uncfcurf  15508  isprs  15559  isdrs  15563  ispos  15576  istos  15665  isdlat  15823  sgrp1  15918  ismhm  15968  issubm  15978  sgrp2nmndlem4  16046  isnsg  16230  isghm  16267  isga  16329  pmtrdifwrdel  16510  sylow2blem2  16641  efglem  16734  efgi  16737  efgredlemb  16764  efgred  16766  frgpuplem  16790  iscmn  16805  ring1  17248  isirred  17348  islmod  17516  lmodlema  17517  lssset  17580  islssd  17582  islmhm  17673  islmhm2  17684  isobs  18751  dmatel  18995  dmatmulcl  19002  scmateALT  19014  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  cpmatel  19212  chpscmat  19343  hausnei2  19854  dfcon2  19920  llyeq  19971  nllyeq  19972  isucn2  20782  iducn  20786  ispsmet  20808  ismet  20826  isxmet  20827  metucnOLD  21091  metucn  21092  ngptgp  21150  nlmvscnlem1  21195  xmetdcn2  21342  addcnlem  21368  elcncf  21393  ipcnlem1  21685  cfili  21707  c1lip1  22398  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou2  22736  aaliou2b  22737  ulmcau  22790  ulmdvlem3  22797  cxpcn3lem  23121  dvdsmulf1o  23470  chpdifbndlem2  23739  pntrsumbnd2  23752  istrkgb  23852  axtgsegcon  23861  axtg5seg  23862  axtgpasch  23864  axtgupdim2  23869  axtgeucl  23870  iscgrg  23904  isismt  23921  isperp2  24092  f1otrg  24174  axcontlem10  24276  axcontlem12  24278  isfrgra  24990  isgrpo  25198  isablo  25285  isass  25318  elghomlem1OLD  25363  elghomlem2OLD  25364  iscom2  25414  vacn  25604  smcnlem  25607  lnoval  25667  islno  25668  isphg  25732  ajmoi  25774  ajval  25777  adjmo  26751  elcnop  26776  ellnop  26777  elunop  26791  elhmop  26792  elcnfn  26801  ellnfn  26802  adjeu  26808  adjval  26809  adj1  26852  adjeq  26854  cnlnadjlem9  26994  cnlnadjeu  26997  cnlnssadj  26999  isst  27132  ishst  27133  cdj1i  27352  cdj3i  27360  resspos  27647  resstos  27648  isomnd  27691  isslmd  27745  slmdlema  27746  isorng  27789  qqhucn  27973  ismntop  28004  txpcon  28677  nofulllem4  29465  nofulllem5  29466  heicant  30049  nn0prpw  30141  equivbnd  30286  isismty  30297  heibor1lem  30305  iccbnd  30336  isrngohom  30368  pridlval  30430  ispridl  30431  isdmn3  30471  ismgmhm  32471  issubmgm  32477  isrnghm  32698  lidlmsgrp  32732  lidlrng  32733  dmatALTbasel  33003  lindslinindsimp2  33064  lmod1  33093  islfl  34785  isopos  34905  psubspset  35468  islaut  35807  ispautN  35823  ltrnset  35842  isltrn  35843  istrnN  35882  istendo  36486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812