Theorem nfbr 5146

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  sbcbr123  5153  nfpo  5539  nfso  5540  pofun  5551  nffr  5598  nfse  5599  nfco  5815  nfcnv  5828  dfdmf  5846  dfrnf  5900  nfdm  5901  dfrel4  6150  dffun6f  6508  nffv  6845  funfv2f  6924  fvopab5  6976  f1ompt  7058  fmptco  7076  nfiso  7270  nfofr  7631  ofrfval2  7645  tposoprab  8206  xpcomco  8999  nfoi  9423  tskwe  9866  cardmin2  9915  uniimadomf  10459  cardmin  10478  inar1  10690  lble  12098  rlim2  15423  ello1mpt  15448  rlimcld2  15505  o1compt  15514  nfsum1  15617  nfsum  15618  fsum00  15725  fsumrlim  15738  o1fsum  15740  nfcprod1  15835  nfcprod  15836  sumeven  16318  sumodd  16319  invfuc  17905  dprd2d2  19979  2ndcdisj  23404  ovoliunlem3  25465  mbfpos  25612  mbfposb  25614  mbfsup  25625  mbfinf  25626  i1fposd  25668  itg2splitlem  25709  itg2split  25710  isibl2  25727  nfitg  25736  cbvitg  25737  itggt0  25805  dvlipcn  25959  dvfsumle  25986  dvfsumleOLD  25987  dvfsumabs  25989  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  rlimcnp  26935  lgamgulmlem2  27000  lgamgulmlem6  27004  dchrisumlema  27459  dchrisumlem2  27461  dchrisumlem3  27462  nosupbnd1  27686  nosupbnd2  27688  noinfbnd1  27701  noinfbnd2  27703  chirred  32474  iundisjf  32667  fmptcof2  32738  fsumiunle  32912  esumfsup  34229  esum2d  34252  measvunilem  34371  measvunilem0  34372  bj-opabco  37395  phpreu  37807  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  itggt0cn  37893  ftc1anclem5  37900  cdleme26ee  40688  cdlemefs32sn1aw  40742  cdleme41sn3a  40761  cdleme32d  40772  cdleme32f  40774  cdlemk38  41243  cdlemk11t  41274  monotoddzz  43252  oddcomabszz  43253  nfrelp  45257  permaxrep  45314  evth2f  45327  evthf  45339  rfcnpre3  45345  rfcnpre4  45346  rfcnnnub  45348  ssfiunibd  45624  uzub  45742  supxrleubrnmptf  45762  infrpgernmpt  45776  monoordxr  45793  monoord2xr  45795  caucvgbf  45800  cvgcaule  45802  fsumlessf  45890  fmul01  45893  fmul01lt1lem1  45897  fmul01lt1  45899  climinff  45924  idlimc  45939  limcperiod  45941  fnlimabslt  45990  limsupref  45996  limsupbnd1f  45997  climbddf  45998  limsuppnfd  46013  climinf2  46018  limsuppnf  46022  limsupubuz  46024  climinf2mpt  46025  climinfmpt  46026  limsupmnf  46032  limsupre2  46036  limsupmnfuz  46038  limsupre3  46044  limsupre3uz  46047  limsupreuz  46048  climuz  46055  limsupgt  46089  liminfreuz  46114  liminflt  46116  xlimpnfxnegmnf  46125  xlimmnf  46152  xlimpnf  46153  dfxlim2  46159  cncfshift  46185  cncficcgt0  46199  stoweidlem3  46314  stoweidlem26  46337  stoweidlem28  46339  stoweidlem31  46342  stoweidlem51  46362  stoweidlem52  46363  stoweidlem59  46370  stirling  46400  fourierdlem20  46438  fourierdlem79  46496  etransclem48  46593  sge0ltfirp  46711  sge0lempt  46721  meaiunincf  46794  iunhoiioolem  46986  pimltmnf2f  47008  pimgtpnf2f  47016  pimltpnf2f  47023  pimgtmnf2  47025  pimdecfgtioc  47026  issmff  47045  smfpimltxrmptf  47069  smfpreimagtf  47079  smflim  47088  smfpimgtxr  47091  smfpimgtxrmptf  47095  smfsup  47125  smfinflem  47128  smfinf  47129  nfafv2  47531  prmdvdsfmtnof1lem1  47897  dffun3f  49994  setrec2  50007