Theorem nfbr 4333

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

Syntax hints:   T. wtru 1365   F/wnf 1594   F/_wnfc 2564   class class class wbr 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290

This theorem is referenced by:  sbcbr123  4340  sbcbrgOLD  4341  nfpo  4642  nfso  4643  pofun  4653  nffr  4690  nfse  4691  nfco  5001  nfcnv  5014  dfdmf  5029  dfrnf  5074  nfdm  5077  dffun6f  5429  nffv  5695  funfv2f  5757  fvopab5  5792  f1ompt  5862  fmptco  5873  nfiso  6012  ofrfval2  6336  tposoprab  6780  xpcomco  7397  nfoi  7724  tskwe  8116  cardmin2  8164  uniimadomf  8705  cardmin  8724  inar1  8938  lble  10278  rlim2  12970  ello1mpt  12995  rlimcld2  13052  o1compt  13061  nfsum1  13163  nfsum  13164  fsum00  13257  fsumrlim  13270  o1fsum  13272  invfuc  14880  dprd2d2  16533  2ndcdisj  19019  ovoliunlem3  20946  mbfpos  21088  mbfposb  21090  mbfsup  21101  mbfinf  21102  i1fposd  21144  itg2splitlem  21185  itg2split  21186  isibl2  21203  nfitg  21211  cbvitg  21212  itggt0  21278  dvlipcn  21425  dvfsumle  21452  dvfsumabs  21454  dvfsumlem2  21458  dvfsumlem4  21460  dvfsumrlim  21462  dvfsum2  21465  rlimcnp  22318  dchrisumlema  22696  dchrisumlem2  22698  dchrisumlem3  22699  chirred  25734  iundisjf  25866  dfrel4  25872  fmptcof2  25914  esumfsup  26455  measvunilem  26562  measvunilem0  26563  lgamgulmlem2  26946  lgamgulmlem6  26950  nfcprod1  27352  nfcprod  27353  itggt0cn  28389  ftc1anclem5  28396  monotoddzz  29209  oddcomabszz  29210  evth2f  29662  evthf  29674  rfcnpre3  29680  rfcnpre4  29681  rfcnnnub  29683  fmul01  29686  fmul01lt1lem1  29690  fmul01lt1  29692  climinff  29709  stoweidlem3  29723  stoweidlem26  29746  stoweidlem28  29748  stoweidlem31  29751  stoweidlem51  29771  stoweidlem52  29772  stoweidlem59  29779  stirling  29809  cdleme26ee  33726  cdlemefs32sn1aw  33780  cdleme41sn3a  33799  cdleme32d  33810  cdleme32f  33812  cdlemk38  34281  cdlemk11t  34312