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  32343  iundisjf  32538  fmptcof2  32608  fsumiunle  32783  esumfsup  34053  esum2d  34076  measvunilem  34195  measvunilem0  34196  bj-opabco  37182  phpreu  37604  poimirlem26  37646  poimirlem27  37647  poimirlem28  37648  itggt0cn  37690  ftc1anclem5  37697  cdleme26ee  40359  cdlemefs32sn1aw  40413  cdleme41sn3a  40432  cdleme32d  40443  cdleme32f  40445  cdlemk38  40914  cdlemk11t  40945  monotoddzz  42936  oddcomabszz  42937  nfrelp  44943  permaxrep  45000  evth2f  45013  evthf  45025  rfcnpre3  45031  rfcnpre4  45032  rfcnnnub  45034  ssfiunibd  45311  uzub  45430  supxrleubrnmptf  45450  infrpgernmpt  45464  monoordxr  45481  monoord2xr  45483  caucvgbf  45488  cvgcaule  45490  fsumlessf  45578  fmul01  45581  fmul01lt1lem1  45585  fmul01lt1  45587  climinff  45612  idlimc  45627  limcperiod  45629  fnlimabslt  45680  limsupref  45686  limsupbnd1f  45687  climbddf  45688  limsuppnfd  45703  climinf2  45708  limsuppnf  45712  limsupubuz  45714  climinf2mpt  45715  climinfmpt  45716  limsupmnf  45722  limsupre2  45726  limsupmnfuz  45728  limsupre3  45734  limsupre3uz  45737  limsupreuz  45738  climuz  45745  limsupgt  45779  liminfreuz  45804  liminflt  45806  xlimpnfxnegmnf  45815  xlimmnf  45842  xlimpnf  45843  dfxlim2  45849  cncfshift  45875  cncficcgt0  45889  stoweidlem3  46004  stoweidlem26  46027  stoweidlem28  46029  stoweidlem31  46032  stoweidlem51  46052  stoweidlem52  46053  stoweidlem59  46060  stirling  46090  fourierdlem20  46128  fourierdlem79  46186  etransclem48  46283  sge0ltfirp  46401  sge0lempt  46411  meaiunincf  46484  iunhoiioolem  46676  pimltmnf2f  46698  pimgtpnf2f  46706  pimltpnf2f  46713  pimgtmnf2  46715  pimdecfgtioc  46716  issmff  46735  smfpimltxrmptf  46759  smfpreimagtf  46769  smflim  46778  smfpimgtxr  46781  smfpimgtxrmptf  46785  smfsup  46815  smfinflem  46818  smfinf  46819  nfafv2  47222  prmdvdsfmtnof1lem1  47588  dffun3f  49687  setrec2  49700