Theorem nfbr 4629

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

Syntax hints:  ⊤wtru 1476  Ⅎwnf 1699  Ⅎwnfc 2738   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  sbcbr123  4636  nfpo  4964  nfso  4965  pofun  4975  nffr  5012  nfse  5013  nfco  5209  nfcnv  5223  dfdmf  5239  dfrnf  5285  nfdm  5288  dfrel4  5504  dffun6f  5818  nffv  6110  funfv2f  6177  fvopab5  6217  f1ompt  6290  fmptco  6303  nfiso  6472  ofrfval2  6813  tposoprab  7275  xpcomco  7935  nfoi  8302  tskwe  8659  cardmin2  8707  uniimadomf  9246  cardmin  9265  inar1  9476  lble  10854  rlim2  14075  ello1mpt  14100  rlimcld2  14157  o1compt  14166  nfsum1  14268  nfsum  14269  fsum00  14371  fsumrlim  14384  o1fsum  14386  nfcprod1  14479  nfcprod  14480  sumeven  14948  sumodd  14949  invfuc  16457  dprd2d2  18266  2ndcdisj  21069  ovoliunlem3  23079  mbfpos  23224  mbfposb  23226  mbfsup  23237  mbfinf  23238  i1fposd  23280  itg2splitlem  23321  itg2split  23322  isibl2  23339  nfitg  23347  cbvitg  23348  itggt0  23414  dvlipcn  23561  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  dvfsumlem4  23596  dvfsumrlim  23598  dvfsum2  23601  rlimcnp  24492  lgamgulmlem2  24556  lgamgulmlem6  24560  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  chirred  28638  iundisjf  28784  fmptcof2  28839  esumfsup  29459  esum2d  29482  measvunilem  29602  measvunilem0  29603  phpreu  32563  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  itggt0cn  32652  ftc1anclem5  32659  cdleme26ee  34666  cdlemefs32sn1aw  34720  cdleme41sn3a  34739  cdleme32d  34750  cdleme32f  34752  cdlemk38  35221  cdlemk11t  35252  monotoddzz  36526  oddcomabszz  36527  evth2f  38197  evthf  38209  rfcnpre3  38215  rfcnpre4  38216  rfcnnnub  38218  ssfiunibd  38464  fsumlessf  38644  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1  38653  climinff  38678  idlimc  38693  limcperiod  38695  fnlimabslt  38746  cncfshift  38759  cncficcgt0  38774  stoweidlem3  38896  stoweidlem26  38919  stoweidlem28  38921  stoweidlem31  38924  stoweidlem51  38944  stoweidlem52  38945  stoweidlem59  38952  stirling  38982  fourierdlem20  39020  fourierdlem79  39078  etransclem48  39175  sge0ltfirp  39293  sge0lempt  39303  iunhoiioolem  39566  pimltmnf2  39588  pimgtpnf2  39594  pimltpnf2  39600  pimgtmnf2  39601  pimdecfgtioc  39602  issmff  39620  smfpimltxrmpt  39645  smfpreimagtf  39654  smflim  39663  smfpimgtxr  39666  smfpimgtxrmpt  39670  prmdvdsfmtnof1lem1  40034  dffun3f  42227  setrec2  42241