Theorem nfbr 5136

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2879   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  sbcbr123  5143  nfpo  5528  nfso  5529  pofun  5540  nffr  5587  nfse  5588  nfco  5804  nfcnv  5817  dfdmf  5835  dfrnf  5889  nfdm  5890  dfrel4  6138  dffun6f  6496  nffv  6832  funfv2f  6911  fvopab5  6962  f1ompt  7044  fmptco  7062  nfiso  7256  nfofr  7617  ofrfval2  7631  tposoprab  8192  xpcomco  8980  nfoi  9400  tskwe  9843  cardmin2  9892  uniimadomf  10436  cardmin  10455  inar1  10666  lble  12074  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  19958  2ndcdisj  23371  ovoliunlem3  25432  mbfpos  25579  mbfposb  25581  mbfsup  25592  mbfinf  25593  i1fposd  25635  itg2splitlem  25676  itg2split  25677  isibl2  25694  nfitg  25703  cbvitg  25704  itggt0  25772  dvlipcn  25926  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem4  25963  dvfsumrlim  25965  dvfsum2  25968  rlimcnp  26902  lgamgulmlem2  26967  lgamgulmlem6  26971  dchrisumlema  27426  dchrisumlem2  27428  dchrisumlem3  27429  nosupbnd1  27653  nosupbnd2  27655  noinfbnd1  27668  noinfbnd2  27670  chirred  32375  iundisjf  32569  fmptcof2  32639  fsumiunle  32812  esumfsup  34083  esum2d  34106  measvunilem  34225  measvunilem0  34226  bj-opabco  37232  phpreu  37643  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  itggt0cn  37729  ftc1anclem5  37736  cdleme26ee  40458  cdlemefs32sn1aw  40512  cdleme41sn3a  40531  cdleme32d  40542  cdleme32f  40544  cdlemk38  41013  cdlemk11t  41044  monotoddzz  43035  oddcomabszz  43036  nfrelp  45041  permaxrep  45098  evth2f  45111  evthf  45123  rfcnpre3  45129  rfcnpre4  45130  rfcnnnub  45132  ssfiunibd  45409  uzub  45528  supxrleubrnmptf  45548  infrpgernmpt  45562  monoordxr  45579  monoord2xr  45581  caucvgbf  45586  cvgcaule  45588  fsumlessf  45676  fmul01  45679  fmul01lt1lem1  45683  fmul01lt1  45685  climinff  45710  idlimc  45725  limcperiod  45727  fnlimabslt  45776  limsupref  45782  limsupbnd1f  45783  climbddf  45784  limsuppnfd  45799  climinf2  45804  limsuppnf  45808  limsupubuz  45810  climinf2mpt  45811  climinfmpt  45812  limsupmnf  45818  limsupre2  45822  limsupmnfuz  45824  limsupre3  45830  limsupre3uz  45833  limsupreuz  45834  climuz  45841  limsupgt  45875  liminfreuz  45900  liminflt  45902  xlimpnfxnegmnf  45911  xlimmnf  45938  xlimpnf  45939  dfxlim2  45945  cncfshift  45971  cncficcgt0  45985  stoweidlem3  46100  stoweidlem26  46123  stoweidlem28  46125  stoweidlem31  46128  stoweidlem51  46148  stoweidlem52  46149  stoweidlem59  46156  stirling  46186  fourierdlem20  46224  fourierdlem79  46282  etransclem48  46379  sge0ltfirp  46497  sge0lempt  46507  meaiunincf  46580  iunhoiioolem  46772  pimltmnf2f  46794  pimgtpnf2f  46802  pimltpnf2f  46809  pimgtmnf2  46811  pimdecfgtioc  46812  issmff  46831  smfpimltxrmptf  46855  smfpreimagtf  46865  smflim  46874  smfpimgtxr  46877  smfpimgtxrmptf  46881  smfsup  46911  smfinflem  46914  smfinf  46915  nfafv2  47317  prmdvdsfmtnof1lem1  47683  dffun3f  49782  setrec2  49795