Theorem nfbr 4461

Description: Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Hypotheses

Ref	Expression
nfbr.1	|- F/_ x A
nfbr.2	|- F/_ x R
nfbr.3	|- F/_ x B

Assertion

Ref	Expression
nfbr	|- F/ x A R B

Proof of Theorem nfbr

Step	Hyp	Ref	Expression
1		nfbr.1	. . . 4 |- F/_ x A
2	1	a1i 11	. . 3 |- ( T. -> F/_ x A )
3		nfbr.2	. . . 4 |- F/_ x R
4	3	a1i 11	. . 3 |- ( T. -> F/_ x R )
5		nfbr.3	. . . 4 |- F/_ x B
6	5	a1i 11	. . 3 |- ( T. -> F/_ x B )
7	2, 4, 6	nfbrd 4460	. 2 |- ( T. -> F/ x A R B )
8	7	trud 1446	1 |- F/ x A R B

Syntax hints:   T. wtru 1438   F/wnf 1663   F/_wnfc 2568   class class class wbr 4417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418

This theorem is referenced by:  sbcbr123  4468  nfpo  4771  nfso  4772  pofun  4782  nffr  4819  nfse  4820  nfco  5011  nfcnv  5024  dfdmf  5039  dfrnf  5084  nfdm  5087  dffun6f  5606  nffv  5879  funfv2f  5941  fvopab5  5980  f1ompt  6050  fmptco  6062  nfiso  6221  ofrfval2  6554  tposoprab  7008  xpcomco  7659  nfoi  8020  tskwe  8374  cardmin2  8422  uniimadomf  8959  cardmin  8978  inar1  9189  lble  10547  rlim2  13527  ello1mpt  13552  rlimcld2  13609  o1compt  13618  nfsum1  13723  nfsum  13724  fsum00  13825  fsumrlim  13838  o1fsum  13840  nfcprod1  13931  nfcprod  13932  invfuc  15823  dprd2d2  17605  2ndcdisj  20395  ovoliunlem3  22331  mbfpos  22481  mbfposb  22483  mbfsup  22494  mbfinf  22495  mbfinfOLD  22496  i1fposd  22539  itg2splitlem  22580  itg2split  22581  isibl2  22598  nfitg  22606  cbvitg  22607  itggt0  22673  dvlipcn  22820  dvfsumle  22847  dvfsumabs  22849  dvfsumlem2  22853  dvfsumlem4  22855  dvfsumrlim  22857  dvfsum2  22860  rlimcnp  23753  lgamgulmlem2  23817  lgamgulmlem6  23821  dchrisumlema  24186  dchrisumlem2  24188  dchrisumlem3  24189  chirred  27880  iundisjf  28035  dfrel4  28044  fmptcof2  28096  esumfsup  28727  esum2d  28750  measvunilem  28870  measvunilem0  28871  phpreu  31633  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  itggt0cn  31718  ftc1anclem5  31725  cdleme26ee  33636  cdlemefs32sn1aw  33690  cdleme41sn3a  33709  cdleme32d  33720  cdleme32f  33722  cdlemk38  34191  cdlemk11t  34222  monotoddzz  35501  oddcomabszz  35502  evth2f  36980  evthf  36992  rfcnpre3  36998  rfcnpre4  36999  rfcnnnub  37001  ssfiunibd  37140  fmul01  37234  fmul01lt1lem1  37238  fmul01lt1  37240  climinff  37266  climinffOLD  37267  idlimc  37282  limcperiod  37284  cncfshift  37327  cncficcgt0  37342  stoweidlem3  37436  stoweidlem26  37459  stoweidlem28  37461  stoweidlem31  37465  stoweidlem51  37485  stoweidlem52  37486  stoweidlem59  37493  stirling  37524  fourierdlem20  37562  fourierdlem79  37621  etransclem48  37718  sge0ltfirp  37780  sge0lempt  37790