NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ralbidv Unicode version

Theorem ralbidv 2634
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1
Assertion
Ref Expression
ralbidv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1619 . 2  F/
2 ralbidv.1 . 2
31, 2ralbid 2632 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176  wral 2614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619
This theorem is referenced by:  ralbii  2638  2ralbidv  2656  rexralbidv  2658  raleqbi1dv  2815  raleqbidv  2819  cbvral2v  2843  rspc2  2960  rspc3v  2964  reu6i  3027  reu7  3031  sbcralt  3118  sbcralg  3120  raaan  3657  raaanv  3658  r19.12sn  3789  2ralunsn  3880  elintg  3934  elintrabg  3939  eliin  3974  nndisjeq  4429  evenodddisjlem1  4515  evenodddisj  4516  nnpweq  4523  ralxpf  4827  funcnvuni  5161  dff4  5421  dff13f  5472  trd  5921  extd  5923  trrd  5925  refrd  5926  refd  5927  nclenn  6249  nnc3n3p1  6278  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem19  6307
  Copyright terms: Public domain W3C validator