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  9881  cardmin2  9930  uniimadomf  10476  cardmin  10495  inar1  10706  lble  12113  rlim2  15439  ello1mpt  15464  rlimcld2  15521  o1compt  15530  nfsum1  15633  nfsum  15634  fsum00  15741  fsumrlim  15754  o1fsum  15756  nfcprod1  15851  nfcprod  15852  sumeven  16334  sumodd  16335  invfuc  17920  dprd2d2  19961  2ndcdisj  23377  ovoliunlem3  25439  mbfpos  25586  mbfposb  25588  mbfsup  25599  mbfinf  25600  i1fposd  25642  itg2splitlem  25683  itg2split  25684  isibl2  25701  nfitg  25710  cbvitg  25711  itggt0  25779  dvlipcn  25933  dvfsumle  25960  dvfsumleOLD  25961  dvfsumabs  25963  dvfsumlem2  25967  dvfsumlem2OLD  25968  dvfsumlem4  25970  dvfsumrlim  25972  dvfsum2  25975  rlimcnp  26909  lgamgulmlem2  26974  lgamgulmlem6  26978  dchrisumlema  27433  dchrisumlem2  27435  dchrisumlem3  27436  nosupbnd1  27660  nosupbnd2  27662  noinfbnd1  27675  noinfbnd2  27677  chirred  32375  iundisjf  32569  fmptcof2  32632  fsumiunle  32805  esumfsup  34054  esum2d  34077  measvunilem  34196  measvunilem0  34197  bj-opabco  37170  phpreu  37592  poimirlem26  37634  poimirlem27  37635  poimirlem28  37636  itggt0cn  37678  ftc1anclem5  37685  cdleme26ee  40348  cdlemefs32sn1aw  40402  cdleme41sn3a  40421  cdleme32d  40432  cdleme32f  40434  cdlemk38  40903  cdlemk11t  40934  monotoddzz  42926  oddcomabszz  42927  nfrelp  44933  permaxrep  44990  evth2f  45003  evthf  45015  rfcnpre3  45021  rfcnpre4  45022  rfcnnnub  45024  ssfiunibd  45301  uzub  45421  supxrleubrnmptf  45441  infrpgernmpt  45455  monoordxr  45472  monoord2xr  45474  caucvgbf  45479  cvgcaule  45481  fsumlessf  45569  fmul01  45572  fmul01lt1lem1  45576  fmul01lt1  45578  climinff  45603  idlimc  45618  limcperiod  45620  fnlimabslt  45671  limsupref  45677  limsupbnd1f  45678  climbddf  45679  limsuppnfd  45694  climinf2  45699  limsuppnf  45703  limsupubuz  45705  climinf2mpt  45706  climinfmpt  45707  limsupmnf  45713  limsupre2  45717  limsupmnfuz  45719  limsupre3  45725  limsupre3uz  45728  limsupreuz  45729  climuz  45736  limsupgt  45770  liminfreuz  45795  liminflt  45797  xlimpnfxnegmnf  45806  xlimmnf  45833  xlimpnf  45834  dfxlim2  45840  cncfshift  45866  cncficcgt0  45880  stoweidlem3  45995  stoweidlem26  46018  stoweidlem28  46020  stoweidlem31  46023  stoweidlem51  46043  stoweidlem52  46044  stoweidlem59  46051  stirling  46081  fourierdlem20  46119  fourierdlem79  46177  etransclem48  46274  sge0ltfirp  46392  sge0lempt  46402  meaiunincf  46475  iunhoiioolem  46667  pimltmnf2f  46689  pimgtpnf2f  46697  pimltpnf2f  46704  pimgtmnf2  46706  pimdecfgtioc  46707  issmff  46726  smfpimltxrmptf  46750  smfpreimagtf  46760  smflim  46769  smfpimgtxr  46772  smfpimgtxrmptf  46776  smfsup  46806  smfinflem  46809  smfinf  46810  nfafv2  47213  prmdvdsfmtnof1lem1  47579  dffun3f  49665  setrec2  49678