Theorem nfbr 4131

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	⊢ Ⅎ𝑥𝐴
nfbr.2	⊢ Ⅎ𝑥𝑅
nfbr.3	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfbr	⊢ Ⅎ𝑥 𝐴𝑅𝐵

Proof of Theorem nfbr

Step	Hyp	Ref	Expression
1		nfbr.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfbr.2	. . . 4 ⊢ Ⅎ𝑥𝑅
4	3	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝑅)
5		nfbr.3	. . . 4 ⊢ Ⅎ𝑥𝐵
6	5	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
7	2, 4, 6	nfbrd 4130	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1404	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1396  Ⅎwnf 1506  Ⅎwnfc 2359   class class class wbr 4084

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4085

This theorem is referenced by:  sbcbrg  4139  nfpo  4394  nfso  4395  pofun  4405  nfse  4434  nffrfor  4441  nfwe  4448  nfco  4891  nfcnv  4905  dfdmf  4920  dfrnf  4969  nfdm  4972  dffun6f  5335  dffun4f  5338  nffv  5643  funfvdm2f  5705  fvmptss2  5715  f1ompt  5792  fmptco  5807  nfiso  5940  nfofr  6235  ofrfval2  6245  tposoprab  6439  modom  6987  xpcomco  7003  nfsup  7180  caucvgprprlemaddq  7916  lble  9115  nfsum1  11904  nfsum  11905  fsum00  12010  mertenslem2  12084  nfcprod1  12102  nfcprod  12103  fprodap0  12169  fprodrec  12177  fproddivapf  12179  fprodap0f  12184  fprodle  12188  oddpwdclemdvds  12729  oddpwdclemndvds  12730