Theorem nfbr 5149

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

Syntax hints:  ⊤wtru 1563  Ⅎwnf 1805  Ⅎwnfc 2911   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  sbcbr123  5156  nfpo  5563  nfso  5564  pofun  5575  nffr  5622  nfse  5623  nfco  5839  nfcnv  5852  dfdmf  5874  dfrnf  5928  nfdm  5929  dfrel4  6179  dffun6f  6538  nffv  6879  funfv2f  6958  fvopab5  7011  f1ompt  7094  fmptco  7113  nfiso  7308  nfofr  7669  ofrfval2  7683  tposoprab  8244  xpcomco  9041  nfoi  9464  tskwe  9910  cardmin2  9959  uniimadomf  10504  cardmin  10523  inar1  10735  lble  12146  rlim2  15525  ello1mpt  15550  rlimcld2  15607  o1compt  15616  nfsum1  15719  nfsum  15720  fsum00  15828  fsumrlim  15841  o1fsum  15843  nfcprod1  15940  nfcprod  15941  sumeven  16423  sumodd  16424  invfuc  18012  dprd2d2  20088  2ndcdisj  23518  ovoliunlem3  25568  mbfpos  25715  mbfposb  25717  mbfsup  25728  mbfinf  25729  i1fposd  25771  itg2splitlem  25812  itg2split  25813  isibl2  25830  nfitg  25839  cbvitg  25840  itggt0  25908  dvlipcn  26058  dvfsumle  26085  dvfsumabs  26087  dvfsumlem2  26091  dvfsumlem4  26093  dvfsumrlim  26095  dvfsum2  26098  rlimcnp  27032  lgamgulmlem2  27096  lgamgulmlem6  27100  dchrisumlema  27554  dchrisumlem2  27556  dchrisumlem3  27557  nosupbnd1  27780  nosupbnd2  27782  noinfbnd1  27795  noinfbnd2  27797  chirred  32600  iundisjf  32791  fmptcof2  32861  fsumiunle  33033  esumfsup  34369  esum2d  34392  measvunilem  34511  measvunilem0  34512  bj-opabco  37685  phpreu  38108  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  itggt0cn  38194  ftc1anclem5  38201  cdleme26ee  40989  cdlemefs32sn1aw  41043  cdleme41sn3a  41062  cdleme32d  41073  cdleme32f  41075  cdlemk38  41544  cdlemk11t  41575  monotoddzz  43525  oddcomabszz  43526  nfrelp  45530  permaxrep  45587  evth2f  45600  evthf  45612  rfcnpre3  45618  rfcnpre4  45619  rfcnnnub  45621  ssfiunibd  45893  uzub  46010  supxrleubrnmptf  46030  infrpgernmpt  46044  monoordxr  46061  monoord2xr  46063  caucvgbf  46068  cvgcaule  46070  fsumlessf  46158  fmul01  46161  fmul01lt1lem1  46165  fmul01lt1  46167  climinff  46192  idlimc  46207  limcperiod  46209  fnlimabslt  46258  limsupref  46264  limsupbnd1f  46265  climbddf  46266  limsuppnfd  46281  climinf2  46286  limsuppnf  46290  limsupubuz  46292  climinf2mpt  46293  climinfmpt  46294  limsupmnf  46300  limsupre2  46304  limsupmnfuz  46306  limsupre3  46312  limsupre3uz  46315  limsupreuz  46316  climuz  46323  limsupgt  46357  liminfreuz  46382  liminflt  46384  xlimpnfxnegmnf  46393  xlimmnf  46420  xlimpnf  46421  dfxlim2  46427  cncfshift  46453  cncficcgt0  46467  stoweidlem3  46582  stoweidlem26  46605  stoweidlem28  46607  stoweidlem31  46610  stoweidlem51  46630  stoweidlem52  46631  stoweidlem59  46638  stirling  46668  fourierdlem20  46706  fourierdlem79  46764  etransclem48  46861  sge0ltfirp  46979  sge0lempt  46989  meaiunincf  47062  iunhoiioolem  47254  pimltmnf2f  47276  pimgtpnf2f  47284  pimltpnf2f  47291  pimgtmnf2  47293  pimdecfgtioc  47294  issmff  47313  smfpimltxrmptf  47337  smfpreimagtf  47347  smflim  47356  smfpimgtxr  47359  smfpimgtxrmptf  47363  smfsup  47393  smfinflem  47396  smfinf  47397  nfafv2  47817  prmdvdsfmtnof1lem1  48198  dffun3f  50308  setrec2  50321