Theorem nfbr 5155

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  sbcbr123  5163  nfpo  5569  nfso  5570  pofun  5581  nffr  5628  nfse  5629  nfco  5848  nfcnv  5862  dfdmf  5884  dfrnf  5938  nfdm  5939  dfrel4  6194  dffun6f  6570  nffv  6915  funfv2f  6994  fvopab5  7047  f1ompt  7132  fmptco  7151  nfiso  7350  nfofr  7721  ofrfval2  7735  tposoprab  8304  xpcomco  9111  nfoi  9532  dffun3f  9999  setrec2  10001  tskwe  10055  cardmin2  10104  uniimadomf  10653  cardmin  10672  inar1  10884  lble  12293  rlim2  15689  ello1mpt  15714  rlimcld2  15771  o1compt  15780  nfsum1  15883  nfsum  15884  fsum00  15991  fsumrlim  16004  o1fsum  16006  nfcprod1  16103  nfcprod  16104  sumeven  16583  sumodd  16584  invfuc  18178  dprd2d2  20287  2ndcdisj  23802  ovoliunlem3  25852  mbfpos  25999  mbfposb  26001  mbfsup  26012  mbfinf  26013  i1fposd  26055  itg2splitlem  26096  itg2split  26097  isibl2  26114  nfitg  26122  cbvitg  26123  itggt0  26191  dvlipcn  26341  dvfsumle  26368  dvfsumabs  26370  dvfsumlem2  26374  dvfsumlem4  26376  dvfsumrlim  26378  dvfsum2  26381  rlimcnp  27320  lgamgulmlem2  27384  lgamgulmlem6  27388  dchrisumlema  27842  dchrisumlem2  27844  dchrisumlem3  27845  nosupbnd1  28098  nosupbnd2  28100  noinfbnd1  28113  noinfbnd2  28115  chirred  33024  iundisjf  33252  fmptcof2  33320  fsumiunle  33487  esumfsup  34769  esum2d  34792  measvunilem  34912  measvunilem0  34913  rankse  35822  bj-opabco  38300  phpreu  38718  poimirlem26  38755  poimirlem27  38756  poimirlem28  38757  itggt0cn  38799  ftc1anclem5  38806  cdleme26ee  41608  cdlemefs32sn1aw  41662  cdleme41sn3a  41681  cdleme32d  41692  cdleme32f  41694  cdlemk38  42163  cdlemk11t  42194  monotoddzz  44141  oddcomabszz  44142  nfrelp  46132  permaxrep  46189  evth2f  46235  evthf  46247  rfcnpre3  46253  rfcnpre4  46254  rfcnnnub  46256  ssfiunibd  46528  uzub  46644  supxrleubrnmptf  46664  infrpgernmpt  46678  monoordxr  46695  monoord2xr  46697  caucvgbf  46702  cvgcaule  46704  fsumlessf  46792  fmul01  46795  fmul01lt1lem1  46799  fmul01lt1  46801  climinff  46826  idlimc  46841  limcperiod  46843  fnlimabslt  46892  limsupref  46898  limsupbnd1f  46899  climbddf  46900  limsuppnfd  46915  climinf2  46920  limsuppnf  46924  limsupubuz  46926  climinf2mpt  46927  climinfmpt  46928  limsupmnf  46934  limsupre2  46938  limsupmnfuz  46940  limsupre3  46946  limsupre3uz  46949  limsupreuz  46950  climuz  46957  limsupgt  46991  liminfreuz  47016  liminflt  47018  xlimpnfxnegmnf  47027  xlimmnf  47054  xlimpnf  47055  dfxlim2  47061  cncfshift  47087  cncficcgt0  47101  stoweidlem3  47216  stoweidlem26  47239  stoweidlem28  47241  stoweidlem31  47244  stoweidlem51  47264  stoweidlem52  47265  stoweidlem59  47272  stirling  47302  fourierdlem20  47340  fourierdlem79  47398  etransclem48  47495  sge0ltfirp  47613  sge0lempt  47623  meaiunincf  47696  iunhoiioolem  47888  pimltmnf2f  47910  pimgtpnf2f  47918  pimltpnf2f  47925  pimgtmnf2  47927  pimdecfgtioc  47928  issmff  47947  smfpimltxrmptf  47971  smfpreimagtf  47981  smflim  47990  smfpimgtxr  47993  smfpimgtxrmptf  47997  smfsup  48027  smfinflem  48030  smfinf  48031  nfafv2  48491  prmdvdsfmtnof1lem1  48872