Theorem nfbr 5144

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2882   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  sbcbr123  5151  nfpo  5537  nfso  5538  pofun  5549  nffr  5596  nfse  5597  nfco  5813  nfcnv  5826  dfdmf  5844  dfrnf  5898  nfdm  5899  dfrel4  6148  dffun6f  6506  nffv  6843  funfv2f  6922  fvopab5  6974  f1ompt  7056  fmptco  7074  nfiso  7268  nfofr  7629  ofrfval2  7643  tposoprab  8204  xpcomco  8997  nfoi  9421  tskwe  9864  cardmin2  9913  uniimadomf  10457  cardmin  10476  inar1  10688  lble  12096  rlim2  15421  ello1mpt  15446  rlimcld2  15503  o1compt  15512  nfsum1  15615  nfsum  15616  fsum00  15723  fsumrlim  15736  o1fsum  15738  nfcprod1  15833  nfcprod  15834  sumeven  16316  sumodd  16317  invfuc  17903  dprd2d2  19977  2ndcdisj  23402  ovoliunlem3  25463  mbfpos  25610  mbfposb  25612  mbfsup  25623  mbfinf  25624  i1fposd  25666  itg2splitlem  25707  itg2split  25708  isibl2  25725  nfitg  25734  cbvitg  25735  itggt0  25803  dvlipcn  25957  dvfsumle  25984  dvfsumleOLD  25985  dvfsumabs  25987  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem4  25994  dvfsumrlim  25996  dvfsum2  25999  rlimcnp  26933  lgamgulmlem2  26998  lgamgulmlem6  27002  dchrisumlema  27457  dchrisumlem2  27459  dchrisumlem3  27460  nosupbnd1  27684  nosupbnd2  27686  noinfbnd1  27699  noinfbnd2  27701  chirred  32451  iundisjf  32644  fmptcof2  32715  fsumiunle  32889  esumfsup  34206  esum2d  34229  measvunilem  34348  measvunilem0  34349  bj-opabco  37362  phpreu  37774  poimirlem26  37816  poimirlem27  37817  poimirlem28  37818  itggt0cn  37860  ftc1anclem5  37867  cdleme26ee  40655  cdlemefs32sn1aw  40709  cdleme41sn3a  40728  cdleme32d  40739  cdleme32f  40741  cdlemk38  41210  cdlemk11t  41241  monotoddzz  43222  oddcomabszz  43223  nfrelp  45227  permaxrep  45284  evth2f  45297  evthf  45309  rfcnpre3  45315  rfcnpre4  45316  rfcnnnub  45318  ssfiunibd  45594  uzub  45712  supxrleubrnmptf  45732  infrpgernmpt  45746  monoordxr  45763  monoord2xr  45765  caucvgbf  45770  cvgcaule  45772  fsumlessf  45860  fmul01  45863  fmul01lt1lem1  45867  fmul01lt1  45869  climinff  45894  idlimc  45909  limcperiod  45911  fnlimabslt  45960  limsupref  45966  limsupbnd1f  45967  climbddf  45968  limsuppnfd  45983  climinf2  45988  limsuppnf  45992  limsupubuz  45994  climinf2mpt  45995  climinfmpt  45996  limsupmnf  46002  limsupre2  46006  limsupmnfuz  46008  limsupre3  46014  limsupre3uz  46017  limsupreuz  46018  climuz  46025  limsupgt  46059  liminfreuz  46084  liminflt  46086  xlimpnfxnegmnf  46095  xlimmnf  46122  xlimpnf  46123  dfxlim2  46129  cncfshift  46155  cncficcgt0  46169  stoweidlem3  46284  stoweidlem26  46307  stoweidlem28  46309  stoweidlem31  46312  stoweidlem51  46332  stoweidlem52  46333  stoweidlem59  46340  stirling  46370  fourierdlem20  46408  fourierdlem79  46466  etransclem48  46563  sge0ltfirp  46681  sge0lempt  46691  meaiunincf  46764  iunhoiioolem  46956  pimltmnf2f  46978  pimgtpnf2f  46986  pimltpnf2f  46993  pimgtmnf2  46995  pimdecfgtioc  46996  issmff  47015  smfpimltxrmptf  47039  smfpreimagtf  47049  smflim  47058  smfpimgtxr  47061  smfpimgtxrmptf  47065  smfsup  47095  smfinflem  47098  smfinf  47099  nfafv2  47501  prmdvdsfmtnof1lem1  47867  dffun3f  49964  setrec2  49977