Theorem nfbr 5122

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

Syntax hints:  ⊤wtru 1549  Ⅎwnf 1791  Ⅎwnfc 2888   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  sbcbr123  5129  nfpo  5535  nfso  5536  pofun  5547  nffr  5594  nfse  5595  nfco  5810  nfcnv  5823  dfdmf  5845  dfrnf  5899  nfdm  5900  dfrel4  6146  dffun6f  6504  nffv  6841  funfv2f  6920  fvopab5  6973  f1ompt  7056  fmptco  7075  nfiso  7270  nfofr  7631  ofrfval2  7645  tposoprab  8206  xpcomco  8999  nfoi  9423  tskwe  9869  cardmin2  9918  uniimadomf  10462  cardmin  10481  inar1  10693  lble  12103  rlim2  15453  ello1mpt  15478  rlimcld2  15535  o1compt  15544  nfsum1  15647  nfsum  15648  fsum00  15756  fsumrlim  15769  o1fsum  15771  nfcprod1  15868  nfcprod  15869  sumeven  16351  sumodd  16352  invfuc  17939  dprd2d2  20016  2ndcdisj  23443  ovoliunlem3  25493  mbfpos  25640  mbfposb  25642  mbfsup  25653  mbfinf  25654  i1fposd  25696  itg2splitlem  25737  itg2split  25738  isibl2  25755  nfitg  25764  cbvitg  25765  itggt0  25833  dvlipcn  25983  dvfsumle  26010  dvfsumabs  26012  dvfsumlem2  26016  dvfsumlem4  26018  dvfsumrlim  26020  dvfsum2  26023  rlimcnp  26951  lgamgulmlem2  27015  lgamgulmlem6  27019  dchrisumlema  27473  dchrisumlem2  27475  dchrisumlem3  27476  nosupbnd1  27700  nosupbnd2  27702  noinfbnd1  27715  noinfbnd2  27717  chirred  32488  iundisjf  32682  fmptcof2  32753  fsumiunle  32925  esumfsup  34266  esum2d  34289  measvunilem  34408  measvunilem0  34409  bj-opabco  37563  phpreu  37986  poimirlem26  38028  poimirlem27  38029  poimirlem28  38030  itggt0cn  38072  ftc1anclem5  38079  cdleme26ee  40867  cdlemefs32sn1aw  40921  cdleme41sn3a  40940  cdleme32d  40951  cdleme32f  40953  cdlemk38  41422  cdlemk11t  41453  monotoddzz  43403  oddcomabszz  43404  nfrelp  45408  permaxrep  45465  evth2f  45478  evthf  45490  rfcnpre3  45496  rfcnpre4  45497  rfcnnnub  45499  ssfiunibd  45771  uzub  45888  supxrleubrnmptf  45908  infrpgernmpt  45922  monoordxr  45939  monoord2xr  45941  caucvgbf  45946  cvgcaule  45948  fsumlessf  46036  fmul01  46039  fmul01lt1lem1  46043  fmul01lt1  46045  climinff  46070  idlimc  46085  limcperiod  46087  fnlimabslt  46136  limsupref  46142  limsupbnd1f  46143  climbddf  46144  limsuppnfd  46159  climinf2  46164  limsuppnf  46168  limsupubuz  46170  climinf2mpt  46171  climinfmpt  46172  limsupmnf  46178  limsupre2  46182  limsupmnfuz  46184  limsupre3  46190  limsupre3uz  46193  limsupreuz  46194  climuz  46201  limsupgt  46235  liminfreuz  46260  liminflt  46262  xlimpnfxnegmnf  46271  xlimmnf  46298  xlimpnf  46299  dfxlim2  46305  cncfshift  46331  cncficcgt0  46345  stoweidlem3  46460  stoweidlem26  46483  stoweidlem28  46485  stoweidlem31  46488  stoweidlem51  46508  stoweidlem52  46509  stoweidlem59  46516  stirling  46546  fourierdlem20  46584  fourierdlem79  46642  etransclem48  46739  sge0ltfirp  46857  sge0lempt  46867  meaiunincf  46940  iunhoiioolem  47132  pimltmnf2f  47154  pimgtpnf2f  47162  pimltpnf2f  47169  pimgtmnf2  47171  pimdecfgtioc  47172  issmff  47191  smfpimltxrmptf  47215  smfpreimagtf  47225  smflim  47234  smfpimgtxr  47237  smfpimgtxrmptf  47241  smfsup  47271  smfinflem  47274  smfinf  47275  nfafv2  47695  prmdvdsfmtnof1lem1  48076  dffun3f  50186  setrec2  50199