Theorem nfbr 4216

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

Syntax hints:   T. wtru 1322   F/wnf 1550   F/_wnfc 2527   class class class wbr 4172

This theorem is referenced by:  sbcbrg  4221  nfpo  4468  nfso  4469  pofun  4479  nffr  4516  nfse  4517  nfco  4997  nfcnv  5010  dfdmf  5023  dfrnf  5067  nfdm  5070  dffun6f  5427  nffv  5694  funfv2f  5751  f1ompt  5850  fmptco  5860  nfiso  6003  ofrfval2  6282  tposoprab  6474  fvopab5  6493  xpcomco  7157  nfoi  7439  tskwe  7793  cardmin2  7841  uniimadomf  8376  cardmin  8395  inar1  8606  lble  9916  rlim2  12245  ello1mpt  12270  rlimcld2  12327  o1compt  12336  nfsum1  12439  nfsum  12440  fsum00  12532  fsumrlim  12545  o1fsum  12547  invfuc  14126  dprd2d2  15557  2ndcdisj  17472  ovoliunlem3  19353  mbfpos  19496  mbfposb  19498  mbfsup  19509  mbfinf  19510  i1fposd  19552  itg2splitlem  19593  itg2split  19594  isibl2  19611  nfitg  19619  cbvitg  19620  itggt0  19686  dvlipcn  19831  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  rlimcnp  20757  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  chirred  23851  iundisjf  23982  dfrel4  23987  fmptcof2  24029  esumfsup  24413  measvunilem  24519  measvunilem0  24520  lgamgulmlem2  24767  lgamgulmlem6  24771  nfcprod1  25189  nfcprod  25190  itggt0cn  26176  monotoddzz  26896  oddcomabszz  26897  evth2f  27553  evthf  27565  rfcnpre3  27571  rfcnpre4  27572  rfcnnnub  27574  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1  27583  climinff  27604  stoweidlem3  27619  stoweidlem26  27642  stoweidlem28  27644  stoweidlem31  27647  stoweidlem51  27667  stoweidlem52  27668  stoweidlem59  27675  stirling  27705  cdleme26ee  30842  cdlemefs32sn1aw  30896  cdleme41sn3a  30915  cdleme32d  30926  cdleme32f  30928  cdlemk38  31397  cdlemk11t  31428

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173