Theorem nfbr 5149

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 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfbr.2	. . . 4 ⊢ Ⅎ𝑥𝑅
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝑅)
5		nfbr.3	. . . 4 ⊢ Ⅎ𝑥𝐵
6	5	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
7	2, 4, 6	nfbrd 5148	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1547	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  sbcbr123  5156  nfpo  5545  nfso  5546  pofun  5557  nffr  5604  nfse  5605  nfco  5819  nfcnv  5832  dfdmf  5850  dfrnf  5903  nfdm  5904  dfrel4  6152  dffun6f  6515  nffv  6850  funfv2f  6932  fvopab5  6983  f1ompt  7065  fmptco  7083  nfiso  7279  nfofr  7640  ofrfval2  7654  tposoprab  8218  xpcomco  9008  nfoi  9443  tskwe  9879  cardmin2  9928  uniimadomf  10474  cardmin  10493  inar1  10704  lble  12111  rlim2  15438  ello1mpt  15463  rlimcld2  15520  o1compt  15529  nfsum1  15632  nfsum  15633  fsum00  15740  fsumrlim  15753  o1fsum  15755  nfcprod1  15850  nfcprod  15851  sumeven  16333  sumodd  16334  invfuc  17919  dprd2d2  19960  2ndcdisj  23376  ovoliunlem3  25438  mbfpos  25585  mbfposb  25587  mbfsup  25598  mbfinf  25599  i1fposd  25641  itg2splitlem  25682  itg2split  25683  isibl2  25700  nfitg  25709  cbvitg  25710  itggt0  25778  dvlipcn  25932  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem4  25969  dvfsumrlim  25971  dvfsum2  25974  rlimcnp  26908  lgamgulmlem2  26973  lgamgulmlem6  26977  dchrisumlema  27432  dchrisumlem2  27434  dchrisumlem3  27435  nosupbnd1  27659  nosupbnd2  27661  noinfbnd1  27674  noinfbnd2  27676  chirred  32374  iundisjf  32568  fmptcof2  32631  fsumiunle  32804  esumfsup  34053  esum2d  34076  measvunilem  34195  measvunilem0  34196  bj-opabco  37169  phpreu  37591  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  itggt0cn  37677  ftc1anclem5  37684  cdleme26ee  40347  cdlemefs32sn1aw  40401  cdleme41sn3a  40420  cdleme32d  40431  cdleme32f  40433  cdlemk38  40902  cdlemk11t  40933  monotoddzz  42925  oddcomabszz  42926  nfrelp  44932  permaxrep  44989  evth2f  45002  evthf  45014  rfcnpre3  45020  rfcnpre4  45021  rfcnnnub  45023  ssfiunibd  45300  uzub  45420  supxrleubrnmptf  45440  infrpgernmpt  45454  monoordxr  45471  monoord2xr  45473  caucvgbf  45478  cvgcaule  45480  fsumlessf  45568  fmul01  45571  fmul01lt1lem1  45575  fmul01lt1  45577  climinff  45602  idlimc  45617  limcperiod  45619  fnlimabslt  45670  limsupref  45676  limsupbnd1f  45677  climbddf  45678  limsuppnfd  45693  climinf2  45698  limsuppnf  45702  limsupubuz  45704  climinf2mpt  45705  climinfmpt  45706  limsupmnf  45712  limsupre2  45716  limsupmnfuz  45718  limsupre3  45724  limsupre3uz  45727  limsupreuz  45728  climuz  45735  limsupgt  45769  liminfreuz  45794  liminflt  45796  xlimpnfxnegmnf  45805  xlimmnf  45832  xlimpnf  45833  dfxlim2  45839  cncfshift  45865  cncficcgt0  45879  stoweidlem3  45994  stoweidlem26  46017  stoweidlem28  46019  stoweidlem31  46022  stoweidlem51  46042  stoweidlem52  46043  stoweidlem59  46050  stirling  46080  fourierdlem20  46118  fourierdlem79  46176  etransclem48  46273  sge0ltfirp  46391  sge0lempt  46401  meaiunincf  46474  iunhoiioolem  46666  pimltmnf2f  46688  pimgtpnf2f  46696  pimltpnf2f  46703  pimgtmnf2  46705  pimdecfgtioc  46706  issmff  46725  smfpimltxrmptf  46749  smfpreimagtf  46759  smflim  46768  smfpimgtxr  46771  smfpimgtxrmptf  46775  smfsup  46805  smfinflem  46808  smfinf  46809  nfafv2  47212  prmdvdsfmtnof1lem1  47578  dffun3f  49664  setrec2  49677