Theorem nfbr 5152

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2907   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  sbcbr123  5159  nfpo  5562  nfso  5563  pofun  5574  nffr  5621  nfse  5622  nfco  5840  nfcnv  5853  dfdmf  5875  dfrnf  5929  nfdm  5930  dfrel4  6179  dffun6f  6543  nffv  6884  funfv2f  6963  fvopab5  7016  f1ompt  7100  fmptco  7119  nfiso  7319  nfofr  7684  ofrfval2  7698  tposoprab  8258  xpcomco  9065  nfoi  9486  dffun3f  9932  setrec2  9934  tskwe  9988  cardmin2  10037  uniimadomf  10586  cardmin  10605  inar1  10817  lble  12224  rlim2  15616  ello1mpt  15641  rlimcld2  15698  o1compt  15707  nfsum1  15810  nfsum  15811  fsum00  15918  fsumrlim  15931  o1fsum  15933  nfcprod1  16030  nfcprod  16031  sumeven  16510  sumodd  16511  invfuc  18099  dprd2d2  20207  2ndcdisj  23722  ovoliunlem3  25772  mbfpos  25919  mbfposb  25921  mbfsup  25932  mbfinf  25933  i1fposd  25975  itg2splitlem  26016  itg2split  26017  isibl2  26034  nfitg  26042  cbvitg  26043  itggt0  26111  dvlipcn  26261  dvfsumle  26288  dvfsumabs  26290  dvfsumlem2  26294  dvfsumlem4  26296  dvfsumrlim  26298  dvfsum2  26301  rlimcnp  27242  lgamgulmlem2  27306  lgamgulmlem6  27310  dchrisumlema  27764  dchrisumlem2  27766  dchrisumlem3  27767  nosupbnd1  27990  nosupbnd2  27992  noinfbnd1  28005  noinfbnd2  28007  chirred  32916  iundisjf  33102  fmptcof2  33170  fsumiunle  33339  esumfsup  34621  esum2d  34644  measvunilem  34764  measvunilem0  34765  bj-opabco  38023  phpreu  38441  poimirlem26  38478  poimirlem27  38479  poimirlem28  38480  itggt0cn  38522  ftc1anclem5  38529  cdleme26ee  41331  cdlemefs32sn1aw  41385  cdleme41sn3a  41404  cdleme32d  41415  cdleme32f  41417  cdlemk38  41886  cdlemk11t  41917  monotoddzz  43882  oddcomabszz  43883  nfrelp  45870  permaxrep  45927  evth2f  45947  evthf  45959  rfcnpre3  45965  rfcnpre4  45966  rfcnnnub  45968  ssfiunibd  46240  uzub  46357  supxrleubrnmptf  46377  infrpgernmpt  46391  monoordxr  46408  monoord2xr  46410  caucvgbf  46415  cvgcaule  46417  fsumlessf  46505  fmul01  46508  fmul01lt1lem1  46512  fmul01lt1  46514  climinff  46539  idlimc  46554  limcperiod  46556  fnlimabslt  46605  limsupref  46611  limsupbnd1f  46612  climbddf  46613  limsuppnfd  46628  climinf2  46633  limsuppnf  46637  limsupubuz  46639  climinf2mpt  46640  climinfmpt  46641  limsupmnf  46647  limsupre2  46651  limsupmnfuz  46653  limsupre3  46659  limsupre3uz  46662  limsupreuz  46663  climuz  46670  limsupgt  46704  liminfreuz  46729  liminflt  46731  xlimpnfxnegmnf  46740  xlimmnf  46767  xlimpnf  46768  dfxlim2  46774  cncfshift  46800  cncficcgt0  46814  stoweidlem3  46929  stoweidlem26  46952  stoweidlem28  46954  stoweidlem31  46957  stoweidlem51  46977  stoweidlem52  46978  stoweidlem59  46985  stirling  47015  fourierdlem20  47053  fourierdlem79  47111  etransclem48  47208  sge0ltfirp  47326  sge0lempt  47336  meaiunincf  47409  iunhoiioolem  47601  pimltmnf2f  47623  pimgtpnf2f  47631  pimltpnf2f  47638  pimgtmnf2  47640  pimdecfgtioc  47641  issmff  47660  smfpimltxrmptf  47684  smfpreimagtf  47694  smflim  47703  smfpimgtxr  47706  smfpimgtxrmptf  47710  smfsup  47740  smfinflem  47743  smfinf  47744  nfafv2  48204  prmdvdsfmtnof1lem1  48585