Theorem nfbr 5195

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786  Ⅎwnfc 2884   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  sbcbr123  5202  nfpo  5593  nfso  5594  pofun  5606  nffr  5650  nfse  5651  nfco  5864  nfcnv  5877  dfdmf  5895  dfrnf  5948  nfdm  5949  dfrel4  6188  dffun6f  6559  nffv  6899  funfv2f  6978  fvopab5  7028  f1ompt  7108  fmptco  7124  nfiso  7316  nfofr  7674  ofrfval2  7688  tposoprab  8244  xpcomco  9059  nfoi  9506  tskwe  9942  cardmin2  9991  uniimadomf  10537  cardmin  10556  inar1  10767  lble  12163  rlim2  15437  ello1mpt  15462  rlimcld2  15519  o1compt  15528  nfsum1  15633  nfsum  15634  fsum00  15741  fsumrlim  15754  o1fsum  15756  nfcprod1  15851  nfcprod  15852  sumeven  16327  sumodd  16328  invfuc  17924  dprd2d2  19909  2ndcdisj  22952  ovoliunlem3  25013  mbfpos  25160  mbfposb  25162  mbfsup  25173  mbfinf  25174  i1fposd  25217  itg2splitlem  25258  itg2split  25259  isibl2  25276  nfitg  25284  cbvitg  25285  itggt0  25353  dvlipcn  25503  dvfsumle  25530  dvfsumabs  25532  dvfsumlem2  25536  dvfsumlem4  25538  dvfsumrlim  25540  dvfsum2  25543  rlimcnp  26460  lgamgulmlem2  26524  lgamgulmlem6  26528  dchrisumlema  26981  dchrisumlem2  26983  dchrisumlem3  26984  nosupbnd1  27207  nosupbnd2  27209  noinfbnd1  27222  noinfbnd2  27224  chirred  31636  iundisjf  31808  fmptcof2  31870  fsumiunle  32023  esumfsup  33057  esum2d  33080  measvunilem  33199  measvunilem0  33200  gg-dvfsumle  35171  gg-dvfsumlem2  35172  bj-opabco  36058  phpreu  36461  poimirlem26  36503  poimirlem27  36504  poimirlem28  36505  itggt0cn  36547  ftc1anclem5  36554  cdleme26ee  39220  cdlemefs32sn1aw  39274  cdleme41sn3a  39293  cdleme32d  39304  cdleme32f  39306  cdlemk38  39775  cdlemk11t  39806  monotoddzz  41668  oddcomabszz  41669  evth2f  43685  evthf  43697  rfcnpre3  43703  rfcnpre4  43704  rfcnnnub  43706  ssfiunibd  44006  uzub  44128  supxrleubrnmptf  44148  infrpgernmpt  44162  monoordxr  44180  monoord2xr  44182  caucvgbf  44187  cvgcaule  44189  fsumlessf  44280  fmul01  44283  fmul01lt1lem1  44287  fmul01lt1  44289  climinff  44314  idlimc  44329  limcperiod  44331  fnlimabslt  44382  limsupref  44388  limsupbnd1f  44389  climbddf  44390  limsuppnfd  44405  climinf2  44410  limsuppnf  44414  limsupubuz  44416  climinf2mpt  44417  climinfmpt  44418  limsupmnf  44424  limsupre2  44428  limsupmnfuz  44430  limsupre3  44436  limsupre3uz  44439  limsupreuz  44440  climuz  44447  limsupgt  44481  liminfreuz  44506  liminflt  44508  xlimpnfxnegmnf  44517  xlimmnf  44544  xlimpnf  44545  dfxlim2  44551  cncfshift  44577  cncficcgt0  44591  stoweidlem3  44706  stoweidlem26  44729  stoweidlem28  44731  stoweidlem31  44734  stoweidlem51  44754  stoweidlem52  44755  stoweidlem59  44762  stirling  44792  fourierdlem20  44830  fourierdlem79  44888  etransclem48  44985  sge0ltfirp  45103  sge0lempt  45113  meaiunincf  45186  iunhoiioolem  45378  pimltmnf2f  45400  pimgtpnf2f  45408  pimltpnf2f  45415  pimgtmnf2  45417  pimdecfgtioc  45418  issmff  45437  smfpimltxrmptf  45461  smfpreimagtf  45471  smflim  45480  smfpimgtxr  45483  smfpimgtxrmptf  45487  smfsup  45517  smfinflem  45520  smfinf  45521  nfafv2  45913  prmdvdsfmtnof1lem1  46239  dffun3f  47681  setrec2  47694