Theorem nfbr 5133

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884   class class class wbr 5086

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  sbcbr123  5140  nfpo  5540  nfso  5541  pofun  5552  nffr  5599  nfse  5600  nfco  5816  nfcnv  5829  dfdmf  5847  dfrnf  5901  nfdm  5902  dfrel4  6151  dffun6f  6509  nffv  6846  funfv2f  6925  fvopab5  6977  f1ompt  7059  fmptco  7078  nfiso  7272  nfofr  7633  ofrfval2  7647  tposoprab  8207  xpcomco  9000  nfoi  9424  tskwe  9869  cardmin2  9918  uniimadomf  10462  cardmin  10481  inar1  10693  lble  12103  rlim2  15453  ello1mpt  15478  rlimcld2  15535  o1compt  15544  nfsum1  15647  nfsum  15648  fsum00  15756  fsumrlim  15769  o1fsum  15771  nfcprod1  15868  nfcprod  15869  sumeven  16351  sumodd  16352  invfuc  17939  dprd2d2  20016  2ndcdisj  23435  ovoliunlem3  25485  mbfpos  25632  mbfposb  25634  mbfsup  25645  mbfinf  25646  i1fposd  25688  itg2splitlem  25729  itg2split  25730  isibl2  25747  nfitg  25756  cbvitg  25757  itggt0  25825  dvlipcn  25975  dvfsumle  26002  dvfsumabs  26004  dvfsumlem2  26008  dvfsumlem4  26010  dvfsumrlim  26012  dvfsum2  26015  rlimcnp  26946  lgamgulmlem2  27011  lgamgulmlem6  27015  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  nosupbnd1  27696  nosupbnd2  27698  noinfbnd1  27711  noinfbnd2  27713  chirred  32485  iundisjf  32678  fmptcof2  32749  fsumiunle  32921  esumfsup  34234  esum2d  34257  measvunilem  34376  measvunilem0  34377  bj-opabco  37522  phpreu  37945  poimirlem26  37987  poimirlem27  37988  poimirlem28  37989  itggt0cn  38031  ftc1anclem5  38038  cdleme26ee  40826  cdlemefs32sn1aw  40880  cdleme41sn3a  40899  cdleme32d  40910  cdleme32f  40912  cdlemk38  41381  cdlemk11t  41412  monotoddzz  43395  oddcomabszz  43396  nfrelp  45400  permaxrep  45457  evth2f  45470  evthf  45482  rfcnpre3  45488  rfcnpre4  45489  rfcnnnub  45491  ssfiunibd  45766  uzub  45883  supxrleubrnmptf  45903  infrpgernmpt  45917  monoordxr  45934  monoord2xr  45936  caucvgbf  45941  cvgcaule  45943  fsumlessf  46031  fmul01  46034  fmul01lt1lem1  46038  fmul01lt1  46040  climinff  46065  idlimc  46080  limcperiod  46082  fnlimabslt  46131  limsupref  46137  limsupbnd1f  46138  climbddf  46139  limsuppnfd  46154  climinf2  46159  limsuppnf  46163  limsupubuz  46165  climinf2mpt  46166  climinfmpt  46167  limsupmnf  46173  limsupre2  46177  limsupmnfuz  46179  limsupre3  46185  limsupre3uz  46188  limsupreuz  46189  climuz  46196  limsupgt  46230  liminfreuz  46255  liminflt  46257  xlimpnfxnegmnf  46266  xlimmnf  46293  xlimpnf  46294  dfxlim2  46300  cncfshift  46326  cncficcgt0  46340  stoweidlem3  46455  stoweidlem26  46478  stoweidlem28  46480  stoweidlem31  46483  stoweidlem51  46503  stoweidlem52  46504  stoweidlem59  46511  stirling  46541  fourierdlem20  46579  fourierdlem79  46637  etransclem48  46734  sge0ltfirp  46852  sge0lempt  46862  meaiunincf  46935  iunhoiioolem  47127  pimltmnf2f  47149  pimgtpnf2f  47157  pimltpnf2f  47164  pimgtmnf2  47166  pimdecfgtioc  47167  issmff  47186  smfpimltxrmptf  47210  smfpreimagtf  47220  smflim  47229  smfpimgtxr  47232  smfpimgtxrmptf  47236  smfsup  47266  smfinflem  47269  smfinf  47270  nfafv2  47684  prmdvdsfmtnof1lem1  48065  dffun3f  50175  setrec2  50188