Theorem nfbr 5157

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2877   class class class wbr 5110

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  sbcbr123  5164  nfpo  5555  nfso  5556  pofun  5567  nffr  5614  nfse  5615  nfco  5832  nfcnv  5845  dfdmf  5863  dfrnf  5917  nfdm  5918  dfrel4  6167  dffun6f  6532  nffv  6871  funfv2f  6953  fvopab5  7004  f1ompt  7086  fmptco  7104  nfiso  7300  nfofr  7663  ofrfval2  7677  tposoprab  8244  xpcomco  9036  nfoi  9474  tskwe  9910  cardmin2  9959  uniimadomf  10505  cardmin  10524  inar1  10735  lble  12142  rlim2  15469  ello1mpt  15494  rlimcld2  15551  o1compt  15560  nfsum1  15663  nfsum  15664  fsum00  15771  fsumrlim  15784  o1fsum  15786  nfcprod1  15881  nfcprod  15882  sumeven  16364  sumodd  16365  invfuc  17946  dprd2d2  19983  2ndcdisj  23350  ovoliunlem3  25412  mbfpos  25559  mbfposb  25561  mbfsup  25572  mbfinf  25573  i1fposd  25615  itg2splitlem  25656  itg2split  25657  isibl2  25674  nfitg  25683  cbvitg  25684  itggt0  25752  dvlipcn  25906  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem4  25943  dvfsumrlim  25945  dvfsum2  25948  rlimcnp  26882  lgamgulmlem2  26947  lgamgulmlem6  26951  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2  27650  chirred  32331  iundisjf  32525  fmptcof2  32588  fsumiunle  32761  esumfsup  34067  esum2d  34090  measvunilem  34209  measvunilem0  34210  bj-opabco  37183  phpreu  37605  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  itggt0cn  37691  ftc1anclem5  37698  cdleme26ee  40361  cdlemefs32sn1aw  40415  cdleme41sn3a  40434  cdleme32d  40445  cdleme32f  40447  cdlemk38  40916  cdlemk11t  40947  monotoddzz  42939  oddcomabszz  42940  nfrelp  44946  permaxrep  45003  evth2f  45016  evthf  45028  rfcnpre3  45034  rfcnpre4  45035  rfcnnnub  45037  ssfiunibd  45314  uzub  45434  supxrleubrnmptf  45454  infrpgernmpt  45468  monoordxr  45485  monoord2xr  45487  caucvgbf  45492  cvgcaule  45494  fsumlessf  45582  fmul01  45585  fmul01lt1lem1  45589  fmul01lt1  45591  climinff  45616  idlimc  45631  limcperiod  45633  fnlimabslt  45684  limsupref  45690  limsupbnd1f  45691  climbddf  45692  limsuppnfd  45707  climinf2  45712  limsuppnf  45716  limsupubuz  45718  climinf2mpt  45719  climinfmpt  45720  limsupmnf  45726  limsupre2  45730  limsupmnfuz  45732  limsupre3  45738  limsupre3uz  45741  limsupreuz  45742  climuz  45749  limsupgt  45783  liminfreuz  45808  liminflt  45810  xlimpnfxnegmnf  45819  xlimmnf  45846  xlimpnf  45847  dfxlim2  45853  cncfshift  45879  cncficcgt0  45893  stoweidlem3  46008  stoweidlem26  46031  stoweidlem28  46033  stoweidlem31  46036  stoweidlem51  46056  stoweidlem52  46057  stoweidlem59  46064  stirling  46094  fourierdlem20  46132  fourierdlem79  46190  etransclem48  46287  sge0ltfirp  46405  sge0lempt  46415  meaiunincf  46488  iunhoiioolem  46680  pimltmnf2f  46702  pimgtpnf2f  46710  pimltpnf2f  46717  pimgtmnf2  46719  pimdecfgtioc  46720  issmff  46739  smfpimltxrmptf  46763  smfpreimagtf  46773  smflim  46782  smfpimgtxr  46785  smfpimgtxrmptf  46789  smfsup  46819  smfinflem  46822  smfinf  46823  nfafv2  47223  prmdvdsfmtnof1lem1  47589  dffun3f  49675  setrec2  49688