Theorem nfbr 5196

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1783  Ⅎwnfc 2881   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  sbcbr123  5203  nfpo  5594  nfso  5595  pofun  5607  nffr  5651  nfse  5652  nfco  5866  nfcnv  5879  dfdmf  5897  dfrnf  5950  nfdm  5951  dfrel4  6191  dffun6f  6562  nffv  6902  funfv2f  6981  fvopab5  7031  f1ompt  7113  fmptco  7130  nfiso  7323  nfofr  7681  ofrfval2  7695  tposoprab  8251  xpcomco  9066  nfoi  9513  tskwe  9949  cardmin2  9998  uniimadomf  10544  cardmin  10563  inar1  10774  lble  12172  rlim2  15446  ello1mpt  15471  rlimcld2  15528  o1compt  15537  nfsum1  15642  nfsum  15643  fsum00  15750  fsumrlim  15763  o1fsum  15765  nfcprod1  15860  nfcprod  15861  sumeven  16336  sumodd  16337  invfuc  17933  dprd2d2  19957  2ndcdisj  23182  ovoliunlem3  25255  mbfpos  25402  mbfposb  25404  mbfsup  25415  mbfinf  25416  i1fposd  25459  itg2splitlem  25500  itg2split  25501  isibl2  25518  nfitg  25526  cbvitg  25527  itggt0  25595  dvlipcn  25745  dvfsumle  25772  dvfsumabs  25774  dvfsumlem2  25778  dvfsumlem4  25780  dvfsumrlim  25782  dvfsum2  25785  rlimcnp  26704  lgamgulmlem2  26768  lgamgulmlem6  26772  dchrisumlema  27225  dchrisumlem2  27227  dchrisumlem3  27228  nosupbnd1  27451  nosupbnd2  27453  noinfbnd1  27466  noinfbnd2  27468  chirred  31913  iundisjf  32085  fmptcof2  32147  fsumiunle  32300  esumfsup  33364  esum2d  33387  measvunilem  33506  measvunilem0  33507  gg-dvfsumle  35470  gg-dvfsumlem2  35471  bj-opabco  36374  phpreu  36777  poimirlem26  36819  poimirlem27  36820  poimirlem28  36821  itggt0cn  36863  ftc1anclem5  36870  cdleme26ee  39536  cdlemefs32sn1aw  39590  cdleme41sn3a  39609  cdleme32d  39620  cdleme32f  39622  cdlemk38  40091  cdlemk11t  40122  monotoddzz  41986  oddcomabszz  41987  evth2f  44003  evthf  44015  rfcnpre3  44021  rfcnpre4  44022  rfcnnnub  44024  ssfiunibd  44319  uzub  44441  supxrleubrnmptf  44461  infrpgernmpt  44475  monoordxr  44493  monoord2xr  44495  caucvgbf  44500  cvgcaule  44502  fsumlessf  44593  fmul01  44596  fmul01lt1lem1  44600  fmul01lt1  44602  climinff  44627  idlimc  44642  limcperiod  44644  fnlimabslt  44695  limsupref  44701  limsupbnd1f  44702  climbddf  44703  limsuppnfd  44718  climinf2  44723  limsuppnf  44727  limsupubuz  44729  climinf2mpt  44730  climinfmpt  44731  limsupmnf  44737  limsupre2  44741  limsupmnfuz  44743  limsupre3  44749  limsupre3uz  44752  limsupreuz  44753  climuz  44760  limsupgt  44794  liminfreuz  44819  liminflt  44821  xlimpnfxnegmnf  44830  xlimmnf  44857  xlimpnf  44858  dfxlim2  44864  cncfshift  44890  cncficcgt0  44904  stoweidlem3  45019  stoweidlem26  45042  stoweidlem28  45044  stoweidlem31  45047  stoweidlem51  45067  stoweidlem52  45068  stoweidlem59  45075  stirling  45105  fourierdlem20  45143  fourierdlem79  45201  etransclem48  45298  sge0ltfirp  45416  sge0lempt  45426  meaiunincf  45499  iunhoiioolem  45691  pimltmnf2f  45713  pimgtpnf2f  45721  pimltpnf2f  45728  pimgtmnf2  45730  pimdecfgtioc  45731  issmff  45750  smfpimltxrmptf  45774  smfpreimagtf  45784  smflim  45793  smfpimgtxr  45796  smfpimgtxrmptf  45800  smfsup  45830  smfinflem  45833  smfinf  45834  nfafv2  46226  prmdvdsfmtnof1lem1  46552  dffun3f  47816  setrec2  47829