Theorem nfbr 5132

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2883   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  sbcbr123  5139  nfpo  5545  nfso  5546  pofun  5557  nffr  5604  nfse  5605  nfco  5820  nfcnv  5833  dfdmf  5851  dfrnf  5905  nfdm  5906  dfrel4  6155  dffun6f  6513  nffv  6850  funfv2f  6929  fvopab5  6981  f1ompt  7063  fmptco  7082  nfiso  7277  nfofr  7638  ofrfval2  7652  tposoprab  8212  xpcomco  9005  nfoi  9429  tskwe  9874  cardmin2  9923  uniimadomf  10467  cardmin  10486  inar1  10698  lble  12108  rlim2  15458  ello1mpt  15483  rlimcld2  15540  o1compt  15549  nfsum1  15652  nfsum  15653  fsum00  15761  fsumrlim  15774  o1fsum  15776  nfcprod1  15873  nfcprod  15874  sumeven  16356  sumodd  16357  invfuc  17944  dprd2d2  20021  2ndcdisj  23421  ovoliunlem3  25471  mbfpos  25618  mbfposb  25620  mbfsup  25631  mbfinf  25632  i1fposd  25674  itg2splitlem  25715  itg2split  25716  isibl2  25733  nfitg  25742  cbvitg  25743  itggt0  25811  dvlipcn  25961  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  rlimcnp  26929  lgamgulmlem2  26993  lgamgulmlem6  26997  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  chirred  32466  iundisjf  32659  fmptcof2  32730  fsumiunle  32902  esumfsup  34214  esum2d  34237  measvunilem  34356  measvunilem0  34357  bj-opabco  37502  phpreu  37925  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  itggt0cn  38011  ftc1anclem5  38018  cdleme26ee  40806  cdlemefs32sn1aw  40860  cdleme41sn3a  40879  cdleme32d  40890  cdleme32f  40892  cdlemk38  41361  cdlemk11t  41392  monotoddzz  43371  oddcomabszz  43372  nfrelp  45376  permaxrep  45433  evth2f  45446  evthf  45458  rfcnpre3  45464  rfcnpre4  45465  rfcnnnub  45467  ssfiunibd  45742  uzub  45859  supxrleubrnmptf  45879  infrpgernmpt  45893  monoordxr  45910  monoord2xr  45912  caucvgbf  45917  cvgcaule  45919  fsumlessf  46007  fmul01  46010  fmul01lt1lem1  46014  fmul01lt1  46016  climinff  46041  idlimc  46056  limcperiod  46058  fnlimabslt  46107  limsupref  46113  limsupbnd1f  46114  climbddf  46115  limsuppnfd  46130  climinf2  46135  limsuppnf  46139  limsupubuz  46141  climinf2mpt  46142  climinfmpt  46143  limsupmnf  46149  limsupre2  46153  limsupmnfuz  46155  limsupre3  46161  limsupre3uz  46164  limsupreuz  46165  climuz  46172  limsupgt  46206  liminfreuz  46231  liminflt  46233  xlimpnfxnegmnf  46242  xlimmnf  46269  xlimpnf  46270  dfxlim2  46276  cncfshift  46302  cncficcgt0  46316  stoweidlem3  46431  stoweidlem26  46454  stoweidlem28  46456  stoweidlem31  46459  stoweidlem51  46479  stoweidlem52  46480  stoweidlem59  46487  stirling  46517  fourierdlem20  46555  fourierdlem79  46613  etransclem48  46710  sge0ltfirp  46828  sge0lempt  46838  meaiunincf  46911  iunhoiioolem  47103  pimltmnf2f  47125  pimgtpnf2f  47133  pimltpnf2f  47140  pimgtmnf2  47142  pimdecfgtioc  47143  issmff  47162  smfpimltxrmptf  47186  smfpreimagtf  47196  smflim  47205  smfpimgtxr  47208  smfpimgtxrmptf  47212  smfsup  47242  smfinflem  47245  smfinf  47246  nfafv2  47666  prmdvdsfmtnof1lem1  48047  dffun3f  50157  setrec2  50170