Theorem nfbr 5192

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

Syntax hints:  ⊤wtru 1535  Ⅎwnf 1778  Ⅎwnfc 2876   class class class wbr 5145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-rab 3421  df-v 3466  df-dif 3951  df-un 3953  df-ss 3965  df-nul 4325  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5146

This theorem is referenced by:  sbcbr123  5199  nfpo  5591  nfso  5592  pofun  5604  nffr  5648  nfse  5649  nfco  5864  nfcnv  5877  dfdmf  5895  dfrnf  5948  nfdm  5949  dfrel4  6194  dffun6f  6563  nffv  6902  funfv2f  6982  fvopab5  7033  f1ompt  7116  fmptco  7134  nfiso  7325  nfofr  7688  ofrfval2  7702  tposoprab  8268  xpcomco  9091  nfoi  9549  tskwe  9985  cardmin2  10034  uniimadomf  10578  cardmin  10597  inar1  10808  lble  12211  rlim2  15492  ello1mpt  15517  rlimcld2  15574  o1compt  15583  nfsum1  15688  nfsum  15689  fsum00  15796  fsumrlim  15809  o1fsum  15811  nfcprod1  15906  nfcprod  15907  sumeven  16383  sumodd  16384  invfuc  17993  dprd2d2  20039  2ndcdisj  23447  ovoliunlem3  25520  mbfpos  25667  mbfposb  25669  mbfsup  25680  mbfinf  25681  i1fposd  25724  itg2splitlem  25765  itg2split  25766  isibl2  25783  nfitg  25791  cbvitg  25792  itggt0  25860  dvlipcn  26014  dvfsumle  26041  dvfsumleOLD  26042  dvfsumabs  26044  dvfsumlem2  26048  dvfsumlem2OLD  26049  dvfsumlem4  26051  dvfsumrlim  26053  dvfsum2  26056  rlimcnp  26989  lgamgulmlem2  27054  lgamgulmlem6  27058  dchrisumlema  27513  dchrisumlem2  27515  dchrisumlem3  27516  nosupbnd1  27740  nosupbnd2  27742  noinfbnd1  27755  noinfbnd2  27757  chirred  32324  iundisjf  32508  fmptcof2  32573  fsumiunle  32732  esumfsup  33915  esum2d  33938  measvunilem  34057  measvunilem0  34058  bj-opabco  36907  phpreu  37317  poimirlem26  37359  poimirlem27  37360  poimirlem28  37361  itggt0cn  37403  ftc1anclem5  37410  cdleme26ee  40071  cdlemefs32sn1aw  40125  cdleme41sn3a  40144  cdleme32d  40155  cdleme32f  40157  cdlemk38  40626  cdlemk11t  40657  monotoddzz  42637  oddcomabszz  42638  evth2f  44650  evthf  44662  rfcnpre3  44668  rfcnpre4  44669  rfcnnnub  44671  ssfiunibd  44959  uzub  45081  supxrleubrnmptf  45101  infrpgernmpt  45115  monoordxr  45133  monoord2xr  45135  caucvgbf  45140  cvgcaule  45142  fsumlessf  45233  fmul01  45236  fmul01lt1lem1  45240  fmul01lt1  45242  climinff  45267  idlimc  45282  limcperiod  45284  fnlimabslt  45335  limsupref  45341  limsupbnd1f  45342  climbddf  45343  limsuppnfd  45358  climinf2  45363  limsuppnf  45367  limsupubuz  45369  climinf2mpt  45370  climinfmpt  45371  limsupmnf  45377  limsupre2  45381  limsupmnfuz  45383  limsupre3  45389  limsupre3uz  45392  limsupreuz  45393  climuz  45400  limsupgt  45434  liminfreuz  45459  liminflt  45461  xlimpnfxnegmnf  45470  xlimmnf  45497  xlimpnf  45498  dfxlim2  45504  cncfshift  45530  cncficcgt0  45544  stoweidlem3  45659  stoweidlem26  45682  stoweidlem28  45684  stoweidlem31  45687  stoweidlem51  45707  stoweidlem52  45708  stoweidlem59  45715  stirling  45745  fourierdlem20  45783  fourierdlem79  45841  etransclem48  45938  sge0ltfirp  46056  sge0lempt  46066  meaiunincf  46139  iunhoiioolem  46331  pimltmnf2f  46353  pimgtpnf2f  46361  pimltpnf2f  46368  pimgtmnf2  46370  pimdecfgtioc  46371  issmff  46390  smfpimltxrmptf  46414  smfpreimagtf  46424  smflim  46433  smfpimgtxr  46436  smfpimgtxrmptf  46440  smfsup  46470  smfinflem  46473  smfinf  46474  nfafv2  46866  prmdvdsfmtnof1lem1  47191  dffun3f  48463  setrec2  48476