Theorem nfbr 4348

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

Syntax hints:   T. wtru 1370   F/wnf 1589   F/_wnfc 2575   class class class wbr 4304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305

This theorem is referenced by:  sbcbr123  4355  sbcbrgOLD  4356  nfpo  4658  nfso  4659  pofun  4669  nffr  4706  nfse  4707  nfco  5017  nfcnv  5030  dfdmf  5045  dfrnf  5090  nfdm  5093  dffun6f  5444  nffv  5710  funfv2f  5772  fvopab5  5807  f1ompt  5877  fmptco  5888  nfiso  6027  ofrfval2  6349  tposoprab  6793  xpcomco  7413  nfoi  7740  tskwe  8132  cardmin2  8180  uniimadomf  8721  cardmin  8740  inar1  8954  lble  10294  rlim2  12986  ello1mpt  13011  rlimcld2  13068  o1compt  13077  nfsum1  13179  nfsum  13180  fsum00  13273  fsumrlim  13286  o1fsum  13288  invfuc  14896  dprd2d2  16555  2ndcdisj  19072  ovoliunlem3  20999  mbfpos  21141  mbfposb  21143  mbfsup  21154  mbfinf  21155  i1fposd  21197  itg2splitlem  21238  itg2split  21239  isibl2  21256  nfitg  21264  cbvitg  21265  itggt0  21331  dvlipcn  21478  dvfsumle  21505  dvfsumabs  21507  dvfsumlem2  21511  dvfsumlem4  21513  dvfsumrlim  21515  dvfsum2  21518  rlimcnp  22371  dchrisumlema  22749  dchrisumlem2  22751  dchrisumlem3  22752  chirred  25811  iundisjf  25943  dfrel4  25949  fmptcof2  25991  esumfsup  26531  measvunilem  26638  measvunilem0  26639  lgamgulmlem2  27028  lgamgulmlem6  27032  nfcprod1  27435  nfcprod  27436  itggt0cn  28476  ftc1anclem5  28483  monotoddzz  29296  oddcomabszz  29297  evth2f  29749  evthf  29761  rfcnpre3  29767  rfcnpre4  29768  rfcnnnub  29770  fmul01  29773  fmul01lt1lem1  29777  fmul01lt1  29779  climinff  29796  stoweidlem3  29810  stoweidlem26  29833  stoweidlem28  29835  stoweidlem31  29838  stoweidlem51  29858  stoweidlem52  29859  stoweidlem59  29866  stirling  29896  cdleme26ee  34016  cdlemefs32sn1aw  34070  cdleme41sn3a  34089  cdleme32d  34100  cdleme32f  34102  cdlemk38  34571  cdlemk11t  34602