Theorem nfbr 5154

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876   class class class wbr 5107

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  sbcbr123  5161  nfpo  5552  nfso  5553  pofun  5564  nffr  5611  nfse  5612  nfco  5829  nfcnv  5842  dfdmf  5860  dfrnf  5914  nfdm  5915  dfrel4  6164  dffun6f  6529  nffv  6868  funfv2f  6950  fvopab5  7001  f1ompt  7083  fmptco  7101  nfiso  7297  nfofr  7660  ofrfval2  7674  tposoprab  8241  xpcomco  9031  nfoi  9467  tskwe  9903  cardmin2  9952  uniimadomf  10498  cardmin  10517  inar1  10728  lble  12135  rlim2  15462  ello1mpt  15487  rlimcld2  15544  o1compt  15553  nfsum1  15656  nfsum  15657  fsum00  15764  fsumrlim  15777  o1fsum  15779  nfcprod1  15874  nfcprod  15875  sumeven  16357  sumodd  16358  invfuc  17939  dprd2d2  19976  2ndcdisj  23343  ovoliunlem3  25405  mbfpos  25552  mbfposb  25554  mbfsup  25565  mbfinf  25566  i1fposd  25608  itg2splitlem  25649  itg2split  25650  isibl2  25667  nfitg  25676  cbvitg  25677  itggt0  25745  dvlipcn  25899  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsumrlim  25938  dvfsum2  25941  rlimcnp  26875  lgamgulmlem2  26940  lgamgulmlem6  26944  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  chirred  32324  iundisjf  32518  fmptcof2  32581  fsumiunle  32754  esumfsup  34060  esum2d  34083  measvunilem  34202  measvunilem0  34203  bj-opabco  37176  phpreu  37598  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  itggt0cn  37684  ftc1anclem5  37691  cdleme26ee  40354  cdlemefs32sn1aw  40408  cdleme41sn3a  40427  cdleme32d  40438  cdleme32f  40440  cdlemk38  40909  cdlemk11t  40940  monotoddzz  42932  oddcomabszz  42933  nfrelp  44939  permaxrep  44996  evth2f  45009  evthf  45021  rfcnpre3  45027  rfcnpre4  45028  rfcnnnub  45030  ssfiunibd  45307  uzub  45427  supxrleubrnmptf  45447  infrpgernmpt  45461  monoordxr  45478  monoord2xr  45480  caucvgbf  45485  cvgcaule  45487  fsumlessf  45575  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1  45584  climinff  45609  idlimc  45624  limcperiod  45626  fnlimabslt  45677  limsupref  45683  limsupbnd1f  45684  climbddf  45685  limsuppnfd  45700  climinf2  45705  limsuppnf  45709  limsupubuz  45711  climinf2mpt  45712  climinfmpt  45713  limsupmnf  45719  limsupre2  45723  limsupmnfuz  45725  limsupre3  45731  limsupre3uz  45734  limsupreuz  45735  climuz  45742  limsupgt  45776  liminfreuz  45801  liminflt  45803  xlimpnfxnegmnf  45812  xlimmnf  45839  xlimpnf  45840  dfxlim2  45846  cncfshift  45872  cncficcgt0  45886  stoweidlem3  46001  stoweidlem26  46024  stoweidlem28  46026  stoweidlem31  46029  stoweidlem51  46049  stoweidlem52  46050  stoweidlem59  46057  stirling  46087  fourierdlem20  46125  fourierdlem79  46183  etransclem48  46280  sge0ltfirp  46398  sge0lempt  46408  meaiunincf  46481  iunhoiioolem  46673  pimltmnf2f  46695  pimgtpnf2f  46703  pimltpnf2f  46710  pimgtmnf2  46712  pimdecfgtioc  46713  issmff  46732  smfpimltxrmptf  46756  smfpreimagtf  46766  smflim  46775  smfpimgtxr  46778  smfpimgtxrmptf  46782  smfsup  46812  smfinflem  46815  smfinf  46816  nfafv2  47219  prmdvdsfmtnof1lem1  47585  dffun3f  49671  setrec2  49684