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  5569  nfso  5570  pofun  5581  nffr  5628  nfse  5629  nfco  5845  nfcnv  5858  dfdmf  5880  dfrnf  5934  nfdm  5935  dfrel4  6184  dffun6f  6548  nffv  6888  funfv2f  6967  fvopab5  7020  f1ompt  7104  fmptco  7123  nfiso  7323  nfofr  7685  ofrfval2  7699  tposoprab  8260  xpcomco  9065  nfoi  9486  tskwe  9955  cardmin2  10004  uniimadomf  10553  cardmin  10572  inar1  10784  lble  12191  rlim2  15583  ello1mpt  15608  rlimcld2  15665  o1compt  15674  nfsum1  15777  nfsum  15778  fsum00  15885  fsumrlim  15898  o1fsum  15900  nfcprod1  15997  nfcprod  15998  sumeven  16477  sumodd  16478  invfuc  18066  dprd2d2  20173  2ndcdisj  23682  ovoliunlem3  25732  mbfpos  25879  mbfposb  25881  mbfsup  25892  mbfinf  25893  i1fposd  25935  itg2splitlem  25976  itg2split  25977  isibl2  25994  nfitg  26002  cbvitg  26003  itggt0  26071  dvlipcn  26221  dvfsumle  26248  dvfsumabs  26250  dvfsumlem2  26254  dvfsumlem4  26256  dvfsumrlim  26258  dvfsum2  26261  rlimcnp  27202  lgamgulmlem2  27266  lgamgulmlem6  27270  dchrisumlema  27724  dchrisumlem2  27726  dchrisumlem3  27727  nosupbnd1  27950  nosupbnd2  27952  noinfbnd1  27965  noinfbnd2  27967  chirred  32876  iundisjf  33062  fmptcof2  33130  fsumiunle  33299  esumfsup  34580  esum2d  34603  measvunilem  34723  measvunilem0  34724  bj-opabco  37940  phpreu  38358  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  itggt0cn  38439  ftc1anclem5  38446  cdleme26ee  41233  cdlemefs32sn1aw  41287  cdleme41sn3a  41306  cdleme32d  41317  cdleme32f  41319  cdlemk38  41788  cdlemk11t  41819  monotoddzz  43784  oddcomabszz  43785  nfrelp  45772  permaxrep  45829  evth2f  45849  evthf  45861  rfcnpre3  45867  rfcnpre4  45868  rfcnnnub  45870  ssfiunibd  46142  uzub  46259  supxrleubrnmptf  46279  infrpgernmpt  46293  monoordxr  46310  monoord2xr  46312  caucvgbf  46317  cvgcaule  46319  fsumlessf  46407  fmul01  46410  fmul01lt1lem1  46414  fmul01lt1  46416  climinff  46441  idlimc  46456  limcperiod  46458  fnlimabslt  46507  limsupref  46513  limsupbnd1f  46514  climbddf  46515  limsuppnfd  46530  climinf2  46535  limsuppnf  46539  limsupubuz  46541  climinf2mpt  46542  climinfmpt  46543  limsupmnf  46549  limsupre2  46553  limsupmnfuz  46555  limsupre3  46561  limsupre3uz  46564  limsupreuz  46565  climuz  46572  limsupgt  46606  liminfreuz  46631  liminflt  46633  xlimpnfxnegmnf  46642  xlimmnf  46669  xlimpnf  46670  dfxlim2  46676  cncfshift  46702  cncficcgt0  46716  stoweidlem3  46831  stoweidlem26  46854  stoweidlem28  46856  stoweidlem31  46859  stoweidlem51  46879  stoweidlem52  46880  stoweidlem59  46887  stirling  46917  fourierdlem20  46955  fourierdlem79  47013  etransclem48  47110  sge0ltfirp  47228  sge0lempt  47238  meaiunincf  47311  iunhoiioolem  47503  pimltmnf2f  47525  pimgtpnf2f  47533  pimltpnf2f  47540  pimgtmnf2  47542  pimdecfgtioc  47543  issmff  47562  smfpimltxrmptf  47586  smfpreimagtf  47596  smflim  47605  smfpimgtxr  47608  smfpimgtxrmptf  47612  smfsup  47642  smfinflem  47645  smfinf  47646  nfafv2  48106  prmdvdsfmtnof1lem1  48487  dffun3f  50608  setrec2  50621