Theorem nfbr 5151

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  sbcbr123  5159  nfpo  5564  nfso  5565  pofun  5576  nffr  5623  nfse  5624  nfco  5842  nfcnv  5855  dfdmf  5877  dfrnf  5931  nfdm  5932  dfrel4  6182  dffun6f  6553  nffv  6895  funfv2f  6974  fvopab5  7027  f1ompt  7111  fmptco  7130  nfiso  7330  nfofr  7700  ofrfval2  7714  tposoprab  8279  xpcomco  9086  nfoi  9508  dffun3f  9975  setrec2  9977  tskwe  10031  cardmin2  10080  uniimadomf  10629  cardmin  10648  inar1  10860  lble  12269  rlim2  15663  ello1mpt  15688  rlimcld2  15745  o1compt  15754  nfsum1  15857  nfsum  15858  fsum00  15965  fsumrlim  15978  o1fsum  15980  nfcprod1  16077  nfcprod  16078  sumeven  16557  sumodd  16558  invfuc  18152  dprd2d2  20260  2ndcdisj  23775  ovoliunlem3  25825  mbfpos  25972  mbfposb  25974  mbfsup  25985  mbfinf  25986  i1fposd  26028  itg2splitlem  26069  itg2split  26070  isibl2  26087  nfitg  26095  cbvitg  26096  itggt0  26164  dvlipcn  26314  dvfsumle  26341  dvfsumabs  26343  dvfsumlem2  26347  dvfsumlem4  26349  dvfsumrlim  26351  dvfsum2  26354  rlimcnp  27293  lgamgulmlem2  27357  lgamgulmlem6  27361  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  nosupbnd1  28071  nosupbnd2  28073  noinfbnd1  28086  noinfbnd2  28088  chirred  32997  iundisjf  33183  fmptcof2  33251  fsumiunle  33420  esumfsup  34702  esum2d  34725  measvunilem  34845  measvunilem0  34846  bj-opabco  38110  phpreu  38528  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  itggt0cn  38609  ftc1anclem5  38616  cdleme26ee  41418  cdlemefs32sn1aw  41472  cdleme41sn3a  41491  cdleme32d  41502  cdleme32f  41504  cdlemk38  41973  cdlemk11t  42004  monotoddzz  43950  oddcomabszz  43951  nfrelp  45939  permaxrep  45996  evth2f  46032  evthf  46044  rfcnpre3  46050  rfcnpre4  46051  rfcnnnub  46053  ssfiunibd  46325  uzub  46441  supxrleubrnmptf  46461  infrpgernmpt  46475  monoordxr  46492  monoord2xr  46494  caucvgbf  46499  cvgcaule  46501  fsumlessf  46589  fmul01  46592  fmul01lt1lem1  46596  fmul01lt1  46598  climinff  46623  idlimc  46638  limcperiod  46640  fnlimabslt  46689  limsupref  46695  limsupbnd1f  46696  climbddf  46697  limsuppnfd  46712  climinf2  46717  limsuppnf  46721  limsupubuz  46723  climinf2mpt  46724  climinfmpt  46725  limsupmnf  46731  limsupre2  46735  limsupmnfuz  46737  limsupre3  46743  limsupre3uz  46746  limsupreuz  46747  climuz  46754  limsupgt  46788  liminfreuz  46813  liminflt  46815  xlimpnfxnegmnf  46824  xlimmnf  46851  xlimpnf  46852  dfxlim2  46858  cncfshift  46884  cncficcgt0  46898  stoweidlem3  47013  stoweidlem26  47036  stoweidlem28  47038  stoweidlem31  47041  stoweidlem51  47061  stoweidlem52  47062  stoweidlem59  47069  stirling  47099  fourierdlem20  47137  fourierdlem79  47195  etransclem48  47292  sge0ltfirp  47410  sge0lempt  47420  meaiunincf  47493  iunhoiioolem  47685  pimltmnf2f  47707  pimgtpnf2f  47715  pimltpnf2f  47722  pimgtmnf2  47724  pimdecfgtioc  47725  issmff  47744  smfpimltxrmptf  47768  smfpreimagtf  47778  smflim  47787  smfpimgtxr  47790  smfpimgtxrmptf  47794  smfsup  47824  smfinflem  47827  smfinf  47828  nfafv2  48288  prmdvdsfmtnof1lem1  48669