Theorem nfbr 5099

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2961   class class class wbr 5052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053

This theorem is referenced by:  sbcbr123  5106  nfpo  5465  nfso  5466  pofun  5477  nffr  5515  nfse  5516  nfco  5722  nfcnv  5735  dfdmf  5751  dfrnf  5806  nfdm  5809  dfrel4  6034  dffun6f  6355  nffv  6666  funfv2f  6738  fvopab5  6786  f1ompt  6861  fmptco  6877  nfiso  7061  nfofr  7401  ofrfval2  7413  tposoprab  7914  xpcomco  8593  nfoi  8964  tskwe  9365  cardmin2  9413  uniimadomf  9953  cardmin  9972  inar1  10183  lble  11579  rlim2  14838  ello1mpt  14863  rlimcld2  14920  o1compt  14929  nfsum1  15031  nfsum  15032  nfsumOLD  15033  fsum00  15138  fsumrlim  15151  o1fsum  15153  nfcprod1  15249  nfcprod  15250  sumeven  15721  sumodd  15722  invfuc  17227  dprd2d2  19149  2ndcdisj  22047  ovoliunlem3  24088  mbfpos  24235  mbfposb  24237  mbfsup  24248  mbfinf  24249  i1fposd  24291  itg2splitlem  24332  itg2split  24333  isibl2  24350  nfitg  24358  cbvitg  24359  itggt0  24427  dvlipcn  24576  dvfsumle  24603  dvfsumabs  24605  dvfsumlem2  24609  dvfsumlem4  24611  dvfsumrlim  24613  dvfsum2  24616  rlimcnp  25529  lgamgulmlem2  25593  lgamgulmlem6  25597  dchrisumlema  26050  dchrisumlem2  26052  dchrisumlem3  26053  chirred  30156  iundisjf  30325  fmptcof2  30388  fsumiunle  30531  esumfsup  31336  esum2d  31359  measvunilem  31478  measvunilem0  31479  nosupbnd1  33221  nosupbnd2  33223  phpreu  34910  poimirlem26  34952  poimirlem27  34953  poimirlem28  34954  itggt0cn  34996  ftc1anclem5  35003  cdleme26ee  37528  cdlemefs32sn1aw  37582  cdleme41sn3a  37601  cdleme32d  37612  cdleme32f  37614  cdlemk38  38083  cdlemk11t  38114  monotoddzz  39632  oddcomabszz  39633  evth2f  41362  evthf  41374  rfcnpre3  41380  rfcnpre4  41381  rfcnnnub  41383  ssfiunibd  41666  uzub  41795  supxrleubrnmptf  41817  infrpgernmpt  41831  monoordxr  41849  monoord2xr  41851  fsumlessf  41948  fmul01  41951  fmul01lt1lem1  41955  fmul01lt1  41957  climinff  41982  idlimc  41997  limcperiod  41999  fnlimabslt  42050  limsupref  42056  limsupbnd1f  42057  climbddf  42058  limsuppnfd  42073  climinf2  42078  limsuppnf  42082  limsupubuz  42084  climinf2mpt  42085  climinfmpt  42086  limsupmnf  42092  limsupre2  42096  limsupmnfuz  42098  limsupre3  42104  limsupre3uz  42107  limsupreuz  42108  climuz  42115  limsupgt  42149  liminfreuz  42174  liminflt  42176  xlimpnfxnegmnf  42185  xlimmnf  42212  xlimpnf  42213  dfxlim2  42219  cncfshift  42247  cncficcgt0  42261  stoweidlem3  42378  stoweidlem26  42401  stoweidlem28  42403  stoweidlem31  42406  stoweidlem51  42426  stoweidlem52  42427  stoweidlem59  42434  stirling  42464  fourierdlem20  42502  fourierdlem79  42560  etransclem48  42657  sge0ltfirp  42772  sge0lempt  42782  meaiunincf  42855  iunhoiioolem  43047  pimltmnf2  43069  pimgtpnf2  43075  pimltpnf2  43081  pimgtmnf2  43082  pimdecfgtioc  43083  issmff  43101  smfpimltxrmpt  43125  smfpreimagtf  43134  smflim  43143  smfpimgtxr  43146  smfpimgtxrmpt  43150  smfsup  43178  smfinflem  43181  smfinf  43182  nfafv2  43507  prmdvdsfmtnof1lem1  43831  dffun3f  44870  setrec2  44883