Theorem nfbr 5190

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2890   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  sbcbr123  5197  nfpo  5598  nfso  5599  pofun  5610  nffr  5658  nfse  5659  nfco  5876  nfcnv  5889  dfdmf  5907  dfrnf  5961  nfdm  5962  dfrel4  6211  dffun6f  6579  nffv  6916  funfv2f  6998  fvopab5  7049  f1ompt  7131  fmptco  7149  nfiso  7342  nfofr  7704  ofrfval2  7718  tposoprab  8287  xpcomco  9102  nfoi  9554  tskwe  9990  cardmin2  10039  uniimadomf  10585  cardmin  10604  inar1  10815  lble  12220  rlim2  15532  ello1mpt  15557  rlimcld2  15614  o1compt  15623  nfsum1  15726  nfsum  15727  fsum00  15834  fsumrlim  15847  o1fsum  15849  nfcprod1  15944  nfcprod  15945  sumeven  16424  sumodd  16425  invfuc  18022  dprd2d2  20064  2ndcdisj  23464  ovoliunlem3  25539  mbfpos  25686  mbfposb  25688  mbfsup  25699  mbfinf  25700  i1fposd  25742  itg2splitlem  25783  itg2split  25784  isibl2  25801  nfitg  25810  cbvitg  25811  itggt0  25879  dvlipcn  26033  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsumrlim  26072  dvfsum2  26075  rlimcnp  27008  lgamgulmlem2  27073  lgamgulmlem6  27077  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  chirred  32414  iundisjf  32602  fmptcof2  32667  fsumiunle  32831  esumfsup  34071  esum2d  34094  measvunilem  34213  measvunilem0  34214  bj-opabco  37189  phpreu  37611  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  itggt0cn  37697  ftc1anclem5  37704  cdleme26ee  40362  cdlemefs32sn1aw  40416  cdleme41sn3a  40435  cdleme32d  40446  cdleme32f  40448  cdlemk38  40917  cdlemk11t  40948  monotoddzz  42955  oddcomabszz  42956  nfrelp  44970  evth2f  45020  evthf  45032  rfcnpre3  45038  rfcnpre4  45039  rfcnnnub  45041  ssfiunibd  45321  uzub  45442  supxrleubrnmptf  45462  infrpgernmpt  45476  monoordxr  45493  monoord2xr  45495  caucvgbf  45500  cvgcaule  45502  fsumlessf  45592  fmul01  45595  fmul01lt1lem1  45599  fmul01lt1  45601  climinff  45626  idlimc  45641  limcperiod  45643  fnlimabslt  45694  limsupref  45700  limsupbnd1f  45701  climbddf  45702  limsuppnfd  45717  climinf2  45722  limsuppnf  45726  limsupubuz  45728  climinf2mpt  45729  climinfmpt  45730  limsupmnf  45736  limsupre2  45740  limsupmnfuz  45742  limsupre3  45748  limsupre3uz  45751  limsupreuz  45752  climuz  45759  limsupgt  45793  liminfreuz  45818  liminflt  45820  xlimpnfxnegmnf  45829  xlimmnf  45856  xlimpnf  45857  dfxlim2  45863  cncfshift  45889  cncficcgt0  45903  stoweidlem3  46018  stoweidlem26  46041  stoweidlem28  46043  stoweidlem31  46046  stoweidlem51  46066  stoweidlem52  46067  stoweidlem59  46074  stirling  46104  fourierdlem20  46142  fourierdlem79  46200  etransclem48  46297  sge0ltfirp  46415  sge0lempt  46425  meaiunincf  46498  iunhoiioolem  46690  pimltmnf2f  46712  pimgtpnf2f  46720  pimltpnf2f  46727  pimgtmnf2  46729  pimdecfgtioc  46730  issmff  46749  smfpimltxrmptf  46773  smfpreimagtf  46783  smflim  46792  smfpimgtxr  46795  smfpimgtxrmptf  46799  smfsup  46829  smfinflem  46832  smfinf  46833  nfafv2  47230  prmdvdsfmtnof1lem1  47571  dffun3f  49201  setrec2  49214