Theorem nfbr 5077

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

Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785  Ⅎwnfc 2936   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  sbcbr123  5084  nfpo  5443  nfso  5444  pofun  5455  nffr  5493  nfse  5494  nfco  5700  nfcnv  5713  dfdmf  5729  dfrnf  5784  nfdm  5787  dfrel4  6015  dffun6f  6338  nffv  6655  funfv2f  6727  fvopab5  6777  f1ompt  6852  fmptco  6868  nfiso  7054  nfofr  7395  ofrfval2  7407  tposoprab  7911  xpcomco  8590  nfoi  8962  tskwe  9363  cardmin2  9412  uniimadomf  9956  cardmin  9975  inar1  10186  lble  11580  rlim2  14845  ello1mpt  14870  rlimcld2  14927  o1compt  14936  nfsum1  15038  nfsum  15039  nfsumOLD  15040  fsum00  15145  fsumrlim  15158  o1fsum  15160  nfcprod1  15256  nfcprod  15257  sumeven  15728  sumodd  15729  invfuc  17236  dprd2d2  19159  2ndcdisj  22061  ovoliunlem3  24108  mbfpos  24255  mbfposb  24257  mbfsup  24268  mbfinf  24269  i1fposd  24311  itg2splitlem  24352  itg2split  24353  isibl2  24370  nfitg  24378  cbvitg  24379  itggt0  24447  dvlipcn  24597  dvfsumle  24624  dvfsumabs  24626  dvfsumlem2  24630  dvfsumlem4  24632  dvfsumrlim  24634  dvfsum2  24637  rlimcnp  25551  lgamgulmlem2  25615  lgamgulmlem6  25619  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  chirred  30178  iundisjf  30352  fmptcof2  30420  fsumiunle  30571  esumfsup  31439  esum2d  31462  measvunilem  31581  measvunilem0  31582  nosupbnd1  33327  nosupbnd2  33329  bj-opabco  34603  phpreu  35041  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  itggt0cn  35127  ftc1anclem5  35134  cdleme26ee  37656  cdlemefs32sn1aw  37710  cdleme41sn3a  37729  cdleme32d  37740  cdleme32f  37742  cdlemk38  38211  cdlemk11t  38242  monotoddzz  39884  oddcomabszz  39885  evth2f  41644  evthf  41656  rfcnpre3  41662  rfcnpre4  41663  rfcnnnub  41665  ssfiunibd  41941  uzub  42068  supxrleubrnmptf  42090  infrpgernmpt  42104  monoordxr  42122  monoord2xr  42124  fsumlessf  42219  fmul01  42222  fmul01lt1lem1  42226  fmul01lt1  42228  climinff  42253  idlimc  42268  limcperiod  42270  fnlimabslt  42321  limsupref  42327  limsupbnd1f  42328  climbddf  42329  limsuppnfd  42344  climinf2  42349  limsuppnf  42353  limsupubuz  42355  climinf2mpt  42356  climinfmpt  42357  limsupmnf  42363  limsupre2  42367  limsupmnfuz  42369  limsupre3  42375  limsupre3uz  42378  limsupreuz  42379  climuz  42386  limsupgt  42420  liminfreuz  42445  liminflt  42447  xlimpnfxnegmnf  42456  xlimmnf  42483  xlimpnf  42484  dfxlim2  42490  cncfshift  42516  cncficcgt0  42530  stoweidlem3  42645  stoweidlem26  42668  stoweidlem28  42670  stoweidlem31  42673  stoweidlem51  42693  stoweidlem52  42694  stoweidlem59  42701  stirling  42731  fourierdlem20  42769  fourierdlem79  42827  etransclem48  42924  sge0ltfirp  43039  sge0lempt  43049  meaiunincf  43122  iunhoiioolem  43314  pimltmnf2  43336  pimgtpnf2  43342  pimltpnf2  43348  pimgtmnf2  43349  pimdecfgtioc  43350  issmff  43368  smfpimltxrmpt  43392  smfpreimagtf  43401  smflim  43410  smfpimgtxr  43413  smfpimgtxrmpt  43417  smfsup  43445  smfinflem  43448  smfinf  43449  nfafv2  43774  prmdvdsfmtnof1lem1  44101  dffun3f  45212  setrec2  45225