Theorem nfbr 4699

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 4698	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	trud 1493	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1484  Ⅎwnf 1708  Ⅎwnfc 2751   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  sbcbr123  4706  nfpo  5040  nfso  5041  pofun  5051  nffr  5088  nfse  5089  nfco  5287  nfcnv  5301  dfdmf  5317  dfrnf  5364  nfdm  5367  dfrel4  5585  dffun6f  5902  nffv  6198  funfv2f  6267  fvopab5  6309  f1ompt  6382  fmptco  6396  nfiso  6572  ofrfval2  6915  tposoprab  7388  xpcomco  8050  nfoi  8419  tskwe  8776  cardmin2  8824  uniimadomf  9367  cardmin  9386  inar1  9597  lble  10975  rlim2  14227  ello1mpt  14252  rlimcld2  14309  o1compt  14318  nfsum1  14420  nfsum  14421  fsum00  14530  fsumrlim  14543  o1fsum  14545  nfcprod1  14640  nfcprod  14641  sumeven  15110  sumodd  15111  invfuc  16634  dprd2d2  18443  2ndcdisj  21259  ovoliunlem3  23272  mbfpos  23418  mbfposb  23420  mbfsup  23431  mbfinf  23432  i1fposd  23474  itg2splitlem  23515  itg2split  23516  isibl2  23533  nfitg  23541  cbvitg  23542  itggt0  23608  dvlipcn  23757  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  dvfsumlem4  23792  dvfsumrlim  23794  dvfsum2  23797  rlimcnp  24692  lgamgulmlem2  24756  lgamgulmlem6  24760  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  chirred  29254  iundisjf  29402  fmptcof2  29457  fsumiunle  29575  esumfsup  30132  esum2d  30155  measvunilem  30275  measvunilem0  30276  nosupbnd1  31860  nosupbnd2  31862  phpreu  33393  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  itggt0cn  33482  ftc1anclem5  33489  cdleme26ee  35648  cdlemefs32sn1aw  35702  cdleme41sn3a  35721  cdleme32d  35732  cdleme32f  35734  cdlemk38  36203  cdlemk11t  36234  monotoddzz  37508  oddcomabszz  37509  evth2f  39174  evthf  39186  rfcnpre3  39192  rfcnpre4  39193  rfcnnnub  39195  ssfiunibd  39523  uzub  39658  supxrleubrnmptf  39680  infrpgernmpt  39695  fsumlessf  39809  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1  39818  climinff  39843  idlimc  39858  limcperiod  39860  fnlimabslt  39911  limsupref  39917  limsupbnd1f  39918  climbddf  39919  limsuppnfd  39934  climinf2  39939  limsuppnf  39943  limsupubuz  39945  climinf2mpt  39946  climinfmpt  39947  limsupmnf  39953  limsupre2  39957  limsupmnfuz  39959  limsupre3  39965  limsupre3uz  39968  limsupreuz  39969  climuz  39976  limsupgt  40010  liminfreuz  40035  liminflt  40037  xlimmnf  40067  xlimpnf  40068  dfxlim2  40074  cncfshift  40087  cncficcgt0  40101  stoweidlem3  40220  stoweidlem26  40243  stoweidlem28  40245  stoweidlem31  40248  stoweidlem51  40268  stoweidlem52  40269  stoweidlem59  40276  stirling  40306  fourierdlem20  40344  fourierdlem79  40402  etransclem48  40499  sge0ltfirp  40617  sge0lempt  40627  iunhoiioolem  40889  pimltmnf2  40911  pimgtpnf2  40917  pimltpnf2  40923  pimgtmnf2  40924  pimdecfgtioc  40925  issmff  40943  smfpimltxrmpt  40967  smfpreimagtf  40976  smflim  40985  smfpimgtxr  40988  smfpimgtxrmpt  40992  smfsup  41020  smfinflem  41023  smfinf  41024  prmdvdsfmtnof1lem1  41496  dffun3f  42429  setrec2  42442