Theorem nfbr 5139

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  sbcbr123  5146  nfpo  5533  nfso  5534  pofun  5545  nffr  5592  nfse  5593  nfco  5808  nfcnv  5821  dfdmf  5839  dfrnf  5892  nfdm  5893  dfrel4  6140  dffun6f  6497  nffv  6832  funfv2f  6912  fvopab5  6963  f1ompt  7045  fmptco  7063  nfiso  7259  nfofr  7620  ofrfval2  7634  tposoprab  8195  xpcomco  8984  nfoi  9406  tskwe  9846  cardmin2  9895  uniimadomf  10439  cardmin  10458  inar1  10669  lble  12077  rlim2  15403  ello1mpt  15428  rlimcld2  15485  o1compt  15494  nfsum1  15597  nfsum  15598  fsum00  15705  fsumrlim  15718  o1fsum  15720  nfcprod1  15815  nfcprod  15816  sumeven  16298  sumodd  16299  invfuc  17884  dprd2d2  19925  2ndcdisj  23341  ovoliunlem3  25403  mbfpos  25550  mbfposb  25552  mbfsup  25563  mbfinf  25564  i1fposd  25606  itg2splitlem  25647  itg2split  25648  isibl2  25665  nfitg  25674  cbvitg  25675  itggt0  25743  dvlipcn  25897  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  dvfsumrlim  25936  dvfsum2  25939  rlimcnp  26873  lgamgulmlem2  26938  lgamgulmlem6  26942  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  nosupbnd1  27624  nosupbnd2  27626  noinfbnd1  27639  noinfbnd2  27641  chirred  32339  iundisjf  32533  fmptcof2  32600  fsumiunle  32774  esumfsup  34037  esum2d  34060  measvunilem  34179  measvunilem0  34180  bj-opabco  37166  phpreu  37588  poimirlem26  37630  poimirlem27  37631  poimirlem28  37632  itggt0cn  37674  ftc1anclem5  37681  cdleme26ee  40343  cdlemefs32sn1aw  40397  cdleme41sn3a  40416  cdleme32d  40427  cdleme32f  40429  cdlemk38  40898  cdlemk11t  40929  monotoddzz  42920  oddcomabszz  42921  nfrelp  44927  permaxrep  44984  evth2f  44997  evthf  45009  rfcnpre3  45015  rfcnpre4  45016  rfcnnnub  45018  ssfiunibd  45295  uzub  45414  supxrleubrnmptf  45434  infrpgernmpt  45448  monoordxr  45465  monoord2xr  45467  caucvgbf  45472  cvgcaule  45474  fsumlessf  45562  fmul01  45565  fmul01lt1lem1  45569  fmul01lt1  45571  climinff  45596  idlimc  45611  limcperiod  45613  fnlimabslt  45664  limsupref  45670  limsupbnd1f  45671  climbddf  45672  limsuppnfd  45687  climinf2  45692  limsuppnf  45696  limsupubuz  45698  climinf2mpt  45699  climinfmpt  45700  limsupmnf  45706  limsupre2  45710  limsupmnfuz  45712  limsupre3  45718  limsupre3uz  45721  limsupreuz  45722  climuz  45729  limsupgt  45763  liminfreuz  45788  liminflt  45790  xlimpnfxnegmnf  45799  xlimmnf  45826  xlimpnf  45827  dfxlim2  45833  cncfshift  45859  cncficcgt0  45873  stoweidlem3  45988  stoweidlem26  46011  stoweidlem28  46013  stoweidlem31  46016  stoweidlem51  46036  stoweidlem52  46037  stoweidlem59  46044  stirling  46074  fourierdlem20  46112  fourierdlem79  46170  etransclem48  46267  sge0ltfirp  46385  sge0lempt  46395  meaiunincf  46468  iunhoiioolem  46660  pimltmnf2f  46682  pimgtpnf2f  46690  pimltpnf2f  46697  pimgtmnf2  46699  pimdecfgtioc  46700  issmff  46719  smfpimltxrmptf  46743  smfpreimagtf  46753  smflim  46762  smfpimgtxr  46765  smfpimgtxrmptf  46769  smfsup  46799  smfinflem  46802  smfinf  46803  nfafv2  47206  prmdvdsfmtnof1lem1  47572  dffun3f  49671  setrec2  49684