Theorem nfbr 5156

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2909   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  sbcbr123  5163  nfpo  5573  nfso  5574  pofun  5585  nffr  5632  nfse  5633  nfco  5849  nfcnv  5862  dfdmf  5884  dfrnf  5938  nfdm  5939  dfrel4  6188  dffun6f  6552  nffv  6892  funfv2f  6971  fvopab5  7024  f1ompt  7107  fmptco  7126  nfiso  7326  nfofr  7688  ofrfval2  7702  tposoprab  8263  xpcomco  9068  nfoi  9489  tskwe  9958  cardmin2  10007  uniimadomf  10556  cardmin  10575  inar1  10787  lble  12194  rlim2  15585  ello1mpt  15610  rlimcld2  15667  o1compt  15676  nfsum1  15779  nfsum  15780  fsum00  15887  fsumrlim  15900  o1fsum  15902  nfcprod1  15999  nfcprod  16000  sumeven  16481  sumodd  16482  invfuc  18070  dprd2d2  20174  2ndcdisj  23683  ovoliunlem3  25733  mbfpos  25880  mbfposb  25882  mbfsup  25893  mbfinf  25894  i1fposd  25936  itg2splitlem  25977  itg2split  25978  isibl2  25995  nfitg  26004  cbvitg  26005  itggt0  26073  dvlipcn  26223  dvfsumle  26250  dvfsumabs  26252  dvfsumlem2  26256  dvfsumlem4  26258  dvfsumrlim  26260  dvfsum2  26263  rlimcnp  27200  lgamgulmlem2  27264  lgamgulmlem6  27268  dchrisumlema  27722  dchrisumlem2  27724  dchrisumlem3  27725  nosupbnd1  27948  nosupbnd2  27950  noinfbnd1  27963  noinfbnd2  27965  chirred  32862  iundisjf  33049  fmptcof2  33117  fsumiunle  33286  esumfsup  34567  esum2d  34590  measvunilem  34710  measvunilem0  34711  bj-opabco  37927  phpreu  38345  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  itggt0cn  38426  ftc1anclem5  38433  cdleme26ee  41220  cdlemefs32sn1aw  41274  cdleme41sn3a  41293  cdleme32d  41304  cdleme32f  41306  cdlemk38  41775  cdlemk11t  41806  monotoddzz  43771  oddcomabszz  43772  nfrelp  45759  permaxrep  45816  evth2f  45836  evthf  45848  rfcnpre3  45854  rfcnpre4  45855  rfcnnnub  45857  ssfiunibd  46129  uzub  46246  supxrleubrnmptf  46266  infrpgernmpt  46280  monoordxr  46297  monoord2xr  46299  caucvgbf  46304  cvgcaule  46306  fsumlessf  46394  fmul01  46397  fmul01lt1lem1  46401  fmul01lt1  46403  climinff  46428  idlimc  46443  limcperiod  46445  fnlimabslt  46494  limsupref  46500  limsupbnd1f  46501  climbddf  46502  limsuppnfd  46517  climinf2  46522  limsuppnf  46526  limsupubuz  46528  climinf2mpt  46529  climinfmpt  46530  limsupmnf  46536  limsupre2  46540  limsupmnfuz  46542  limsupre3  46548  limsupre3uz  46551  limsupreuz  46552  climuz  46559  limsupgt  46593  liminfreuz  46618  liminflt  46620  xlimpnfxnegmnf  46629  xlimmnf  46656  xlimpnf  46657  dfxlim2  46663  cncfshift  46689  cncficcgt0  46703  stoweidlem3  46818  stoweidlem26  46841  stoweidlem28  46843  stoweidlem31  46846  stoweidlem51  46866  stoweidlem52  46867  stoweidlem59  46874  stirling  46904  fourierdlem20  46942  fourierdlem79  47000  etransclem48  47097  sge0ltfirp  47215  sge0lempt  47225  meaiunincf  47298  iunhoiioolem  47490  pimltmnf2f  47512  pimgtpnf2f  47520  pimltpnf2f  47527  pimgtmnf2  47529  pimdecfgtioc  47530  issmff  47549  smfpimltxrmptf  47573  smfpreimagtf  47583  smflim  47592  smfpimgtxr  47595  smfpimgtxrmptf  47599  smfsup  47629  smfinflem  47632  smfinf  47633  nfafv2  48093  prmdvdsfmtnof1lem1  48474  dffun3f  50595  setrec2  50608