Theorem nfbr 5213

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781  Ⅎwnfc 2893   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  sbcbr123  5220  nfpo  5613  nfso  5614  pofun  5626  nffr  5673  nfse  5674  nfco  5890  nfcnv  5903  dfdmf  5921  dfrnf  5975  nfdm  5976  dfrel4  6222  dffun6f  6591  nffv  6930  funfv2f  7011  fvopab5  7062  f1ompt  7145  fmptco  7163  nfiso  7358  nfofr  7721  ofrfval2  7735  tposoprab  8303  xpcomco  9128  nfoi  9583  tskwe  10019  cardmin2  10068  uniimadomf  10614  cardmin  10633  inar1  10844  lble  12247  rlim2  15542  ello1mpt  15567  rlimcld2  15624  o1compt  15633  nfsum1  15738  nfsum  15739  fsum00  15846  fsumrlim  15859  o1fsum  15861  nfcprod1  15956  nfcprod  15957  sumeven  16435  sumodd  16436  invfuc  18044  dprd2d2  20088  2ndcdisj  23485  ovoliunlem3  25558  mbfpos  25705  mbfposb  25707  mbfsup  25718  mbfinf  25719  i1fposd  25762  itg2splitlem  25803  itg2split  25804  isibl2  25821  nfitg  25830  cbvitg  25831  itggt0  25899  dvlipcn  26053  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem4  26090  dvfsumrlim  26092  dvfsum2  26095  rlimcnp  27026  lgamgulmlem2  27091  lgamgulmlem6  27095  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  nosupbnd1  27777  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2  27794  chirred  32427  iundisjf  32611  fmptcof2  32675  fsumiunle  32833  esumfsup  34034  esum2d  34057  measvunilem  34176  measvunilem0  34177  bj-opabco  37154  phpreu  37564  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  itggt0cn  37650  ftc1anclem5  37657  cdleme26ee  40317  cdlemefs32sn1aw  40371  cdleme41sn3a  40390  cdleme32d  40401  cdleme32f  40403  cdlemk38  40872  cdlemk11t  40903  monotoddzz  42900  oddcomabszz  42901  evth2f  44915  evthf  44927  rfcnpre3  44933  rfcnpre4  44934  rfcnnnub  44936  ssfiunibd  45224  uzub  45346  supxrleubrnmptf  45366  infrpgernmpt  45380  monoordxr  45398  monoord2xr  45400  caucvgbf  45405  cvgcaule  45407  fsumlessf  45498  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1  45507  climinff  45532  idlimc  45547  limcperiod  45549  fnlimabslt  45600  limsupref  45606  limsupbnd1f  45607  climbddf  45608  limsuppnfd  45623  climinf2  45628  limsuppnf  45632  limsupubuz  45634  climinf2mpt  45635  climinfmpt  45636  limsupmnf  45642  limsupre2  45646  limsupmnfuz  45648  limsupre3  45654  limsupre3uz  45657  limsupreuz  45658  climuz  45665  limsupgt  45699  liminfreuz  45724  liminflt  45726  xlimpnfxnegmnf  45735  xlimmnf  45762  xlimpnf  45763  dfxlim2  45769  cncfshift  45795  cncficcgt0  45809  stoweidlem3  45924  stoweidlem26  45947  stoweidlem28  45949  stoweidlem31  45952  stoweidlem51  45972  stoweidlem52  45973  stoweidlem59  45980  stirling  46010  fourierdlem20  46048  fourierdlem79  46106  etransclem48  46203  sge0ltfirp  46321  sge0lempt  46331  meaiunincf  46404  iunhoiioolem  46596  pimltmnf2f  46618  pimgtpnf2f  46626  pimltpnf2f  46633  pimgtmnf2  46635  pimdecfgtioc  46636  issmff  46655  smfpimltxrmptf  46679  smfpreimagtf  46689  smflim  46698  smfpimgtxr  46701  smfpimgtxrmptf  46705  smfsup  46735  smfinflem  46738  smfinf  46739  nfafv2  47133  prmdvdsfmtnof1lem1  47458  dffun3f  48774  setrec2  48787