Theorem nfbr 4933

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

Syntax hints:  ⊤wtru 1602  Ⅎwnf 1827  Ⅎwnfc 2919   class class class wbr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887

This theorem is referenced by:  sbcbr123  4940  nfpo  5279  nfso  5280  pofun  5291  nffr  5329  nfse  5330  nfco  5533  nfcnv  5546  dfdmf  5562  dfrnf  5610  nfdm  5613  dfrel4  5839  dffun6f  6149  nffv  6456  funfv2f  6527  fvopab5  6572  f1ompt  6645  fmptco  6661  nfiso  6844  nfofr  7180  ofrfval2  7192  tposoprab  7670  xpcomco  8338  nfoi  8708  tskwe  9109  cardmin2  9157  uniimadomf  9702  cardmin  9721  inar1  9932  lble  11329  rlim2  14635  ello1mpt  14660  rlimcld2  14717  o1compt  14726  nfsum1  14828  nfsum  14829  fsum00  14934  fsumrlim  14947  o1fsum  14949  nfcprod1  15043  nfcprod  15044  sumeven  15517  sumodd  15518  invfuc  17019  dprd2d2  18830  2ndcdisj  21668  ovoliunlem3  23708  mbfpos  23855  mbfposb  23857  mbfsup  23868  mbfinf  23869  i1fposd  23911  itg2splitlem  23952  itg2split  23953  isibl2  23970  nfitg  23978  cbvitg  23979  itggt0  24045  dvlipcn  24194  dvfsumle  24221  dvfsumabs  24223  dvfsumlem2  24227  dvfsumlem4  24229  dvfsumrlim  24231  dvfsum2  24234  rlimcnp  25144  lgamgulmlem2  25208  lgamgulmlem6  25212  dchrisumlema  25629  dchrisumlem2  25631  dchrisumlem3  25632  chirred  29826  iundisjf  29965  fmptcof2  30022  fsumiunle  30139  esumfsup  30730  esum2d  30753  measvunilem  30873  measvunilem0  30874  nosupbnd1  32449  nosupbnd2  32451  phpreu  34018  poimirlem26  34061  poimirlem27  34062  poimirlem28  34063  itggt0cn  34107  ftc1anclem5  34114  cdleme26ee  36514  cdlemefs32sn1aw  36568  cdleme41sn3a  36587  cdleme32d  36598  cdleme32f  36600  cdlemk38  37069  cdlemk11t  37100  monotoddzz  38467  oddcomabszz  38468  evth2f  40107  evthf  40119  rfcnpre3  40125  rfcnpre4  40126  rfcnnnub  40128  ssfiunibd  40432  uzub  40564  supxrleubrnmptf  40586  infrpgernmpt  40600  monoordxr  40618  monoord2xr  40620  fsumlessf  40717  fmul01  40720  fmul01lt1lem1  40724  fmul01lt1  40726  climinff  40751  idlimc  40766  limcperiod  40768  fnlimabslt  40819  limsupref  40825  limsupbnd1f  40826  climbddf  40827  limsuppnfd  40842  climinf2  40847  limsuppnf  40851  limsupubuz  40853  climinf2mpt  40854  climinfmpt  40855  limsupmnf  40861  limsupre2  40865  limsupmnfuz  40867  limsupre3  40873  limsupre3uz  40876  limsupreuz  40877  climuz  40884  limsupgt  40918  liminfreuz  40943  liminflt  40945  xlimpnfxnegmnf  40954  xlimmnf  40981  xlimpnf  40982  dfxlim2  40988  cncfshift  41015  cncficcgt0  41029  stoweidlem3  41147  stoweidlem26  41170  stoweidlem28  41172  stoweidlem31  41175  stoweidlem51  41195  stoweidlem52  41196  stoweidlem59  41203  stirling  41233  fourierdlem20  41271  fourierdlem79  41329  etransclem48  41426  sge0ltfirp  41541  sge0lempt  41551  meaiunincf  41624  iunhoiioolem  41816  pimltmnf2  41838  pimgtpnf2  41844  pimltpnf2  41850  pimgtmnf2  41851  pimdecfgtioc  41852  issmff  41870  smfpimltxrmpt  41894  smfpreimagtf  41903  smflim  41912  smfpimgtxr  41915  smfpimgtxrmpt  41919  smfsup  41947  smfinflem  41950  smfinf  41951  nfafv2  42259  prmdvdsfmtnof1lem1  42517  dffun3f  43534  setrec2  43547