Theorem nfbr 5117

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  sbcbr123  5124  nfpo  5499  nfso  5500  pofun  5512  nffr  5554  nfse  5555  nfco  5763  nfcnv  5776  dfdmf  5794  dfrnf  5848  nfdm  5849  dfrel4  6083  dffun6f  6432  nffv  6766  funfv2f  6839  fvopab5  6889  f1ompt  6967  fmptco  6983  nfiso  7173  nfofr  7518  ofrfval2  7532  tposoprab  8049  xpcomco  8802  nfoi  9203  tskwe  9639  cardmin2  9688  uniimadomf  10232  cardmin  10251  inar1  10462  lble  11857  rlim2  15133  ello1mpt  15158  rlimcld2  15215  o1compt  15224  nfsum1  15329  nfsum  15330  nfsumOLD  15331  fsum00  15438  fsumrlim  15451  o1fsum  15453  nfcprod1  15548  nfcprod  15549  sumeven  16024  sumodd  16025  invfuc  17608  dprd2d2  19562  2ndcdisj  22515  ovoliunlem3  24573  mbfpos  24720  mbfposb  24722  mbfsup  24733  mbfinf  24734  i1fposd  24777  itg2splitlem  24818  itg2split  24819  isibl2  24836  nfitg  24844  cbvitg  24845  itggt0  24913  dvlipcn  25063  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim  25100  dvfsum2  25103  rlimcnp  26020  lgamgulmlem2  26084  lgamgulmlem6  26088  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  chirred  30658  iundisjf  30829  fmptcof2  30896  fsumiunle  31045  esumfsup  31938  esum2d  31961  measvunilem  32080  measvunilem0  32081  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  bj-opabco  35286  phpreu  35688  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  itggt0cn  35774  ftc1anclem5  35781  cdleme26ee  38301  cdlemefs32sn1aw  38355  cdleme41sn3a  38374  cdleme32d  38385  cdleme32f  38387  cdlemk38  38856  cdlemk11t  38887  monotoddzz  40681  oddcomabszz  40682  evth2f  42447  evthf  42459  rfcnpre3  42465  rfcnpre4  42466  rfcnnnub  42468  ssfiunibd  42738  uzub  42861  supxrleubrnmptf  42881  infrpgernmpt  42895  monoordxr  42913  monoord2xr  42915  fsumlessf  43008  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1  43017  climinff  43042  idlimc  43057  limcperiod  43059  fnlimabslt  43110  limsupref  43116  limsupbnd1f  43117  climbddf  43118  limsuppnfd  43133  climinf2  43138  limsuppnf  43142  limsupubuz  43144  climinf2mpt  43145  climinfmpt  43146  limsupmnf  43152  limsupre2  43156  limsupmnfuz  43158  limsupre3  43164  limsupre3uz  43167  limsupreuz  43168  climuz  43175  limsupgt  43209  liminfreuz  43234  liminflt  43236  xlimpnfxnegmnf  43245  xlimmnf  43272  xlimpnf  43273  dfxlim2  43279  cncfshift  43305  cncficcgt0  43319  stoweidlem3  43434  stoweidlem26  43457  stoweidlem28  43459  stoweidlem31  43462  stoweidlem51  43482  stoweidlem52  43483  stoweidlem59  43490  stirling  43520  fourierdlem20  43558  fourierdlem79  43616  etransclem48  43713  sge0ltfirp  43828  sge0lempt  43838  meaiunincf  43911  iunhoiioolem  44103  pimltmnf2  44125  pimgtpnf2  44131  pimltpnf2  44137  pimgtmnf2  44138  pimdecfgtioc  44139  issmff  44157  smfpimltxrmpt  44181  smfpreimagtf  44190  smflim  44199  smfpimgtxr  44202  smfpimgtxrmpt  44206  smfsup  44234  smfinflem  44237  smfinf  44238  nfafv2  44597  prmdvdsfmtnof1lem1  44924  dffun3f  46274  setrec2  46287