Theorem nfbr 5122

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786  Ⅎwnfc 2888   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  sbcbr123  5129  nfpo  5509  nfso  5510  pofun  5522  nffr  5564  nfse  5565  nfco  5777  nfcnv  5790  dfdmf  5808  dfrnf  5862  nfdm  5863  dfrel4  6099  dffun6f  6454  nffv  6793  funfv2f  6866  fvopab5  6916  f1ompt  6994  fmptco  7010  nfiso  7202  nfofr  7549  ofrfval2  7563  tposoprab  8087  xpcomco  8858  nfoi  9282  tskwe  9717  cardmin2  9766  uniimadomf  10310  cardmin  10329  inar1  10540  lble  11936  rlim2  15214  ello1mpt  15239  rlimcld2  15296  o1compt  15305  nfsum1  15410  nfsum  15411  nfsumOLD  15412  fsum00  15519  fsumrlim  15532  o1fsum  15534  nfcprod1  15629  nfcprod  15630  sumeven  16105  sumodd  16106  invfuc  17701  dprd2d2  19656  2ndcdisj  22616  ovoliunlem3  24677  mbfpos  24824  mbfposb  24826  mbfsup  24837  mbfinf  24838  i1fposd  24881  itg2splitlem  24922  itg2split  24923  isibl2  24940  nfitg  24948  cbvitg  24949  itggt0  25017  dvlipcn  25167  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  dvfsumlem4  25202  dvfsumrlim  25204  dvfsum2  25207  rlimcnp  26124  lgamgulmlem2  26188  lgamgulmlem6  26192  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  chirred  30766  iundisjf  30937  fmptcof2  31003  fsumiunle  31152  esumfsup  32047  esum2d  32070  measvunilem  32189  measvunilem0  32190  nosupbnd1  33926  nosupbnd2  33928  noinfbnd1  33941  noinfbnd2  33943  bj-opabco  35368  phpreu  35770  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  itggt0cn  35856  ftc1anclem5  35863  cdleme26ee  38381  cdlemefs32sn1aw  38435  cdleme41sn3a  38454  cdleme32d  38465  cdleme32f  38467  cdlemk38  38936  cdlemk11t  38967  monotoddzz  40772  oddcomabszz  40773  evth2f  42565  evthf  42577  rfcnpre3  42583  rfcnpre4  42584  rfcnnnub  42586  ssfiunibd  42855  uzub  42978  supxrleubrnmptf  42998  infrpgernmpt  43012  monoordxr  43030  monoord2xr  43032  fsumlessf  43125  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1  43134  climinff  43159  idlimc  43174  limcperiod  43176  fnlimabslt  43227  limsupref  43233  limsupbnd1f  43234  climbddf  43235  limsuppnfd  43250  climinf2  43255  limsuppnf  43259  limsupubuz  43261  climinf2mpt  43262  climinfmpt  43263  limsupmnf  43269  limsupre2  43273  limsupmnfuz  43275  limsupre3  43281  limsupre3uz  43284  limsupreuz  43285  climuz  43292  limsupgt  43326  liminfreuz  43351  liminflt  43353  xlimpnfxnegmnf  43362  xlimmnf  43389  xlimpnf  43390  dfxlim2  43396  cncfshift  43422  cncficcgt0  43436  stoweidlem3  43551  stoweidlem26  43574  stoweidlem28  43576  stoweidlem31  43579  stoweidlem51  43599  stoweidlem52  43600  stoweidlem59  43607  stirling  43637  fourierdlem20  43675  fourierdlem79  43733  etransclem48  43830  sge0ltfirp  43945  sge0lempt  43955  meaiunincf  44028  iunhoiioolem  44220  pimltmnf2f  44242  pimgtpnf2f  44250  pimltpnf2f  44257  pimgtmnf2  44259  pimdecfgtioc  44260  issmff  44279  smfpimltxrmptf  44303  smfpreimagtf  44313  smflim  44322  smfpimgtxr  44325  smfpimgtxrmptf  44329  smfsup  44358  smfinflem  44361  smfinf  44362  nfafv2  44721  prmdvdsfmtnof1lem1  45047  dffun3f  46399  setrec2  46412