Theorem nfbr 5166

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2883   class class class wbr 5119

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  sbcbr123  5173  nfpo  5567  nfso  5568  pofun  5579  nffr  5627  nfse  5628  nfco  5845  nfcnv  5858  dfdmf  5876  dfrnf  5930  nfdm  5931  dfrel4  6180  dffun6f  6548  nffv  6885  funfv2f  6967  fvopab5  7018  f1ompt  7100  fmptco  7118  nfiso  7314  nfofr  7676  ofrfval2  7690  tposoprab  8259  xpcomco  9074  nfoi  9526  tskwe  9962  cardmin2  10011  uniimadomf  10557  cardmin  10576  inar1  10787  lble  12192  rlim2  15510  ello1mpt  15535  rlimcld2  15592  o1compt  15601  nfsum1  15704  nfsum  15705  fsum00  15812  fsumrlim  15825  o1fsum  15827  nfcprod1  15922  nfcprod  15923  sumeven  16404  sumodd  16405  invfuc  17988  dprd2d2  20025  2ndcdisj  23392  ovoliunlem3  25455  mbfpos  25602  mbfposb  25604  mbfsup  25615  mbfinf  25616  i1fposd  25658  itg2splitlem  25699  itg2split  25700  isibl2  25717  nfitg  25726  cbvitg  25727  itggt0  25795  dvlipcn  25949  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem4  25986  dvfsumrlim  25988  dvfsum2  25991  rlimcnp  26925  lgamgulmlem2  26990  lgamgulmlem6  26994  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  nosupbnd1  27676  nosupbnd2  27678  noinfbnd1  27691  noinfbnd2  27693  chirred  32322  iundisjf  32516  fmptcof2  32581  fsumiunle  32754  esumfsup  34047  esum2d  34070  measvunilem  34189  measvunilem0  34190  bj-opabco  37152  phpreu  37574  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  itggt0cn  37660  ftc1anclem5  37667  cdleme26ee  40325  cdlemefs32sn1aw  40379  cdleme41sn3a  40398  cdleme32d  40409  cdleme32f  40411  cdlemk38  40880  cdlemk11t  40911  monotoddzz  42914  oddcomabszz  42915  nfrelp  44922  permaxrep  44979  evth2f  44987  evthf  44999  rfcnpre3  45005  rfcnpre4  45006  rfcnnnub  45008  ssfiunibd  45286  uzub  45406  supxrleubrnmptf  45426  infrpgernmpt  45440  monoordxr  45457  monoord2xr  45459  caucvgbf  45464  cvgcaule  45466  fsumlessf  45554  fmul01  45557  fmul01lt1lem1  45561  fmul01lt1  45563  climinff  45588  idlimc  45603  limcperiod  45605  fnlimabslt  45656  limsupref  45662  limsupbnd1f  45663  climbddf  45664  limsuppnfd  45679  climinf2  45684  limsuppnf  45688  limsupubuz  45690  climinf2mpt  45691  climinfmpt  45692  limsupmnf  45698  limsupre2  45702  limsupmnfuz  45704  limsupre3  45710  limsupre3uz  45713  limsupreuz  45714  climuz  45721  limsupgt  45755  liminfreuz  45780  liminflt  45782  xlimpnfxnegmnf  45791  xlimmnf  45818  xlimpnf  45819  dfxlim2  45825  cncfshift  45851  cncficcgt0  45865  stoweidlem3  45980  stoweidlem26  46003  stoweidlem28  46005  stoweidlem31  46008  stoweidlem51  46028  stoweidlem52  46029  stoweidlem59  46036  stirling  46066  fourierdlem20  46104  fourierdlem79  46162  etransclem48  46259  sge0ltfirp  46377  sge0lempt  46387  meaiunincf  46460  iunhoiioolem  46652  pimltmnf2f  46674  pimgtpnf2f  46682  pimltpnf2f  46689  pimgtmnf2  46691  pimdecfgtioc  46692  issmff  46711  smfpimltxrmptf  46735  smfpreimagtf  46745  smflim  46754  smfpimgtxr  46757  smfpimgtxrmptf  46761  smfsup  46791  smfinflem  46794  smfinf  46795  nfafv2  47195  prmdvdsfmtnof1lem1  47546  dffun3f  49494  setrec2  49507