Theorem nfbr 5194

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

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1779  Ⅎwnfc 2887   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  sbcbr123  5201  nfpo  5602  nfso  5603  pofun  5614  nffr  5661  nfse  5662  nfco  5878  nfcnv  5891  dfdmf  5909  dfrnf  5963  nfdm  5964  dfrel4  6212  dffun6f  6580  nffv  6916  funfv2f  6997  fvopab5  7048  f1ompt  7130  fmptco  7148  nfiso  7341  nfofr  7703  ofrfval2  7717  tposoprab  8285  xpcomco  9100  nfoi  9551  tskwe  9987  cardmin2  10036  uniimadomf  10582  cardmin  10601  inar1  10812  lble  12217  rlim2  15528  ello1mpt  15553  rlimcld2  15610  o1compt  15619  nfsum1  15722  nfsum  15723  fsum00  15830  fsumrlim  15843  o1fsum  15845  nfcprod1  15940  nfcprod  15941  sumeven  16420  sumodd  16421  invfuc  18030  dprd2d2  20078  2ndcdisj  23479  ovoliunlem3  25552  mbfpos  25699  mbfposb  25701  mbfsup  25712  mbfinf  25713  i1fposd  25756  itg2splitlem  25797  itg2split  25798  isibl2  25815  nfitg  25824  cbvitg  25825  itggt0  25893  dvlipcn  26047  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  dvfsumrlim  26086  dvfsum2  26089  rlimcnp  27022  lgamgulmlem2  27087  lgamgulmlem6  27091  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  nosupbnd1  27773  nosupbnd2  27775  noinfbnd1  27788  noinfbnd2  27790  chirred  32423  iundisjf  32608  fmptcof2  32673  fsumiunle  32835  esumfsup  34050  esum2d  34073  measvunilem  34192  measvunilem0  34193  bj-opabco  37170  phpreu  37590  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  itggt0cn  37676  ftc1anclem5  37683  cdleme26ee  40342  cdlemefs32sn1aw  40396  cdleme41sn3a  40415  cdleme32d  40426  cdleme32f  40428  cdlemk38  40897  cdlemk11t  40928  monotoddzz  42931  oddcomabszz  42932  evth2f  44952  evthf  44964  rfcnpre3  44970  rfcnpre4  44971  rfcnnnub  44973  ssfiunibd  45259  uzub  45380  supxrleubrnmptf  45400  infrpgernmpt  45414  monoordxr  45432  monoord2xr  45434  caucvgbf  45439  cvgcaule  45441  fsumlessf  45532  fmul01  45535  fmul01lt1lem1  45539  fmul01lt1  45541  climinff  45566  idlimc  45581  limcperiod  45583  fnlimabslt  45634  limsupref  45640  limsupbnd1f  45641  climbddf  45642  limsuppnfd  45657  climinf2  45662  limsuppnf  45666  limsupubuz  45668  climinf2mpt  45669  climinfmpt  45670  limsupmnf  45676  limsupre2  45680  limsupmnfuz  45682  limsupre3  45688  limsupre3uz  45691  limsupreuz  45692  climuz  45699  limsupgt  45733  liminfreuz  45758  liminflt  45760  xlimpnfxnegmnf  45769  xlimmnf  45796  xlimpnf  45797  dfxlim2  45803  cncfshift  45829  cncficcgt0  45843  stoweidlem3  45958  stoweidlem26  45981  stoweidlem28  45983  stoweidlem31  45986  stoweidlem51  46006  stoweidlem52  46007  stoweidlem59  46014  stirling  46044  fourierdlem20  46082  fourierdlem79  46140  etransclem48  46237  sge0ltfirp  46355  sge0lempt  46365  meaiunincf  46438  iunhoiioolem  46630  pimltmnf2f  46652  pimgtpnf2f  46660  pimltpnf2f  46667  pimgtmnf2  46669  pimdecfgtioc  46670  issmff  46689  smfpimltxrmptf  46713  smfpreimagtf  46723  smflim  46732  smfpimgtxr  46735  smfpimgtxrmptf  46739  smfsup  46769  smfinflem  46772  smfinf  46773  nfafv2  47167  prmdvdsfmtnof1lem1  47508  dffun3f  48912  setrec2  48925