Theorem nfbr 4447

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

Syntax hints:   T. wtru 1445   F/wnf 1667   F/_wnfc 2579   class class class wbr 4402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403

This theorem is referenced by:  sbcbr123  4454  nfpo  4760  nfso  4761  pofun  4771  nffr  4808  nfse  4809  nfco  5000  nfcnv  5013  dfdmf  5028  dfrnf  5073  nfdm  5076  dffun6f  5596  nffv  5872  funfv2f  5934  fvopab5  5974  f1ompt  6044  fmptco  6056  nfiso  6215  ofrfval2  6549  tposoprab  7009  xpcomco  7662  nfoi  8029  tskwe  8384  cardmin2  8432  uniimadomf  8970  cardmin  8989  inar1  9200  lble  10558  rlim2  13560  ello1mpt  13585  rlimcld2  13642  o1compt  13651  nfsum1  13756  nfsum  13757  fsum00  13858  fsumrlim  13871  o1fsum  13873  nfcprod1  13964  nfcprod  13965  invfuc  15879  dprd2d2  17677  2ndcdisj  20471  ovoliunlem3  22457  mbfpos  22607  mbfposb  22609  mbfsup  22620  mbfinf  22621  mbfinfOLD  22622  i1fposd  22665  itg2splitlem  22706  itg2split  22707  isibl2  22724  nfitg  22732  cbvitg  22733  itggt0  22799  dvlipcn  22946  dvfsumle  22973  dvfsumabs  22975  dvfsumlem2  22979  dvfsumlem4  22981  dvfsumrlim  22983  dvfsum2  22986  rlimcnp  23891  lgamgulmlem2  23955  lgamgulmlem6  23959  dchrisumlema  24326  dchrisumlem2  24328  dchrisumlem3  24329  chirred  28048  iundisjf  28199  dfrel4  28208  fmptcof2  28259  esumfsup  28891  esum2d  28914  measvunilem  29034  measvunilem0  29035  phpreu  31929  poimirlem26  31966  poimirlem27  31967  poimirlem28  31968  itggt0cn  32014  ftc1anclem5  32021  cdleme26ee  33927  cdlemefs32sn1aw  33981  cdleme41sn3a  34000  cdleme32d  34011  cdleme32f  34013  cdlemk38  34482  cdlemk11t  34513  monotoddzz  35791  oddcomabszz  35792  evth2f  37336  evthf  37348  rfcnpre3  37354  rfcnpre4  37355  rfcnnnub  37357  ssfiunibd  37527  fsumlessf  37656  fmul01  37658  fmul01lt1lem1  37662  fmul01lt1  37664  climinff  37690  climinffOLD  37691  idlimc  37706  limcperiod  37708  cncfshift  37751  cncficcgt0  37766  stoweidlem3  37863  stoweidlem26  37886  stoweidlem28  37888  stoweidlem31  37892  stoweidlem51  37912  stoweidlem52  37913  stoweidlem59  37920  stirling  37951  fourierdlem20  37989  fourierdlem79  38049  etransclem48OLD  38147  etransclem48  38148  sge0ltfirp  38242  sge0lempt  38252