Theorem nfbr 4491

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 4490	. 2 |- ( T. -> F/ x A R B )
8	7	trud 1388	1 |- F/ x A R B

Syntax hints:   T. wtru 1380   F/wnf 1599   F/_wnfc 2615   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448

This theorem is referenced by:  sbcbr123  4498  sbcbrgOLD  4499  nfpo  4805  nfso  4806  pofun  4816  nffr  4853  nfse  4854  nfco  5167  nfcnv  5180  dfdmf  5195  dfrnf  5240  nfdm  5243  dffun6f  5601  nffv  5872  funfv2f  5935  fvopab5  5972  f1ompt  6042  fmptco  6053  nfiso  6207  ofrfval2  6540  tposoprab  6991  xpcomco  7607  nfoi  7938  tskwe  8330  cardmin2  8378  uniimadomf  8919  cardmin  8938  inar1  9152  lble  10494  rlim2  13281  ello1mpt  13306  rlimcld2  13363  o1compt  13372  nfsum1  13474  nfsum  13475  fsum00  13574  fsumrlim  13587  o1fsum  13589  invfuc  15200  dprd2d2  16892  2ndcdisj  19739  ovoliunlem3  21666  mbfpos  21809  mbfposb  21811  mbfsup  21822  mbfinf  21823  i1fposd  21865  itg2splitlem  21906  itg2split  21907  isibl2  21924  nfitg  21932  cbvitg  21933  itggt0  21999  dvlipcn  22146  dvfsumle  22173  dvfsumabs  22175  dvfsumlem2  22179  dvfsumlem4  22181  dvfsumrlim  22183  dvfsum2  22186  rlimcnp  23039  dchrisumlema  23417  dchrisumlem2  23419  dchrisumlem3  23420  chirred  27006  iundisjf  27137  dfrel4  27143  fmptcof2  27190  esumfsup  27732  measvunilem  27839  measvunilem0  27840  lgamgulmlem2  28228  lgamgulmlem6  28232  nfcprod1  28635  nfcprod  28636  itggt0cn  29680  ftc1anclem5  29687  monotoddzz  30499  oddcomabszz  30500  evth2f  30984  evthf  30996  rfcnpre3  31002  rfcnpre4  31003  rfcnnnub  31005  ssfiunibd  31102  fmul01  31146  fmul01lt1lem1  31150  fmul01lt1  31152  climinff  31169  idlimc  31184  limcperiod  31186  cncfshift  31228  cncficcgt0  31243  stoweidlem3  31319  stoweidlem26  31342  stoweidlem28  31344  stoweidlem31  31347  stoweidlem51  31367  stoweidlem52  31368  stoweidlem59  31375  stirling  31405  fourierdlem20  31443  fourierdlem79  31502  cdleme26ee  35165  cdlemefs32sn1aw  35219  cdleme41sn3a  35238  cdleme32d  35249  cdleme32f  35251  cdlemk38  35720  cdlemk11t  35751