Theorem nfbr 4010

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 9	. . 3 |- ( T. -> F/_ x A )
3		nfbr.2	. . . 4 |- F/_ x R
4	3	a1i 9	. . 3 |- ( T. -> F/_ x R )
5		nfbr.3	. . . 4 |- F/_ x B
6	5	a1i 9	. . 3 |- ( T. -> F/_ x B )
7	2, 4, 6	nfbrd 4009	. 2 |- ( T. -> F/ x A R B )
8	7	mptru 1344	1 |- F/ x A R B

Syntax hints:   T. wtru 1336   F/wnf 1440   F/_wnfc 2286   class class class wbr 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-br 3966

This theorem is referenced by:  sbcbrg  4018  nfpo  4261  nfso  4262  pofun  4272  nfse  4301  nffrfor  4308  nfwe  4315  nfco  4750  nfcnv  4764  dfdmf  4778  dfrnf  4826  nfdm  4829  dffun6f  5182  dffun4f  5185  nffv  5477  funfvdm2f  5532  fvmptss2  5542  f1ompt  5617  fmptco  5632  nfiso  5753  nfofr  6035  ofrfval2  6045  tposoprab  6224  xpcomco  6768  nfsup  6933  caucvgprprlemaddq  7623  lble  8813  nfsum1  11248  nfsum  11249  fsum00  11354  mertenslem2  11428  nfcprod1  11446  nfcprod  11447  fprodap0  11513  fprodrec  11521  fproddivapf  11523  fprodap0f  11528  fprodle  11532  oddpwdclemdvds  12039  oddpwdclemndvds  12040