Theorem nfbr 4172

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 4171	. 2 |- ( T. -> F/ x A R B )
8	7	mptru 1411	1 |- F/ x A R B

Syntax hints:   T. wtru 1403   F/wnf 1513   F/_wnfc 2379   class class class wbr 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  sbcbrg  4180  nfpo  4441  nfso  4442  pofun  4452  nfse  4481  nffrfor  4488  nfwe  4495  nfco  4940  nfcnv  4954  dfdmf  4969  dfrnf  5018  nfdm  5021  dffun6f  5385  dffun4f  5388  nffv  5700  funfvdm2f  5762  fvmptss2  5774  f1ompt  5850  fmptco  5865  nfiso  6002  nfofr  6299  ofrfval2  6309  tposoprab  6541  modom  7098  xpcomco  7114  nfsup  7322  caucvgprprlemaddq  8065  lble  9267  nfsum1  12100  nfsum  12101  fsum00  12207  mertenslem2  12281  nfcprod1  12299  nfcprod  12300  fprodap0  12366  fprodrec  12374  fproddivapf  12376  fprodap0f  12381  fprodle  12385  oddpwdclemdvds  12926  oddpwdclemndvds  12927