Theorem nfbr 4133

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 4132	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1404	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

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

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 4087

This theorem is referenced by:  sbcbrg  4141  nfpo  4396  nfso  4397  pofun  4407  nfse  4436  nffrfor  4443  nfwe  4450  nfco  4893  nfcnv  4907  dfdmf  4922  dfrnf  4971  nfdm  4974  dffun6f  5337  dffun4f  5340  nffv  5645  funfvdm2f  5707  fvmptss2  5717  f1ompt  5794  fmptco  5809  nfiso  5942  nfofr  6237  ofrfval2  6247  tposoprab  6441  modom  6989  xpcomco  7005  nfsup  7182  caucvgprprlemaddq  7918  lble  9117  nfsum1  11907  nfsum  11908  fsum00  12013  mertenslem2  12087  nfcprod1  12105  nfcprod  12106  fprodap0  12172  fprodrec  12180  fproddivapf  12182  fprodap0f  12187  fprodle  12191  oddpwdclemdvds  12732  oddpwdclemndvds  12733