MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfbr Structured version   Visualization version   GIF version

Theorem nfbr 4659
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
StepHypRef Expression
1 nfbr.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfbr.2 . . . 4 𝑥𝑅
43a1i 11 . . 3 (⊤ → 𝑥𝑅)
5 nfbr.3 . . . 4 𝑥𝐵
65a1i 11 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfbrd 4658 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87trud 1490 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnf 1705  wnfc 2748   class class class wbr 4613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614
This theorem is referenced by:  sbcbr123  4666  nfpo  5000  nfso  5001  pofun  5011  nffr  5048  nfse  5049  nfco  5247  nfcnv  5261  dfdmf  5277  dfrnf  5324  nfdm  5327  dfrel4  5544  dffun6f  5861  nffv  6155  funfv2f  6224  fvopab5  6265  f1ompt  6338  fmptco  6351  nfiso  6526  ofrfval2  6868  tposoprab  7333  xpcomco  7994  nfoi  8363  tskwe  8720  cardmin2  8768  uniimadomf  9311  cardmin  9330  inar1  9541  lble  10919  rlim2  14161  ello1mpt  14186  rlimcld2  14243  o1compt  14252  nfsum1  14354  nfsum  14355  fsum00  14457  fsumrlim  14470  o1fsum  14472  nfcprod1  14565  nfcprod  14566  sumeven  15034  sumodd  15035  invfuc  16555  dprd2d2  18364  2ndcdisj  21169  ovoliunlem3  23179  mbfpos  23324  mbfposb  23326  mbfsup  23337  mbfinf  23338  i1fposd  23380  itg2splitlem  23421  itg2split  23422  isibl2  23439  nfitg  23447  cbvitg  23448  itggt0  23514  dvlipcn  23661  dvfsumle  23688  dvfsumabs  23690  dvfsumlem2  23694  dvfsumlem4  23696  dvfsumrlim  23698  dvfsum2  23701  rlimcnp  24592  lgamgulmlem2  24656  lgamgulmlem6  24660  dchrisumlema  25077  dchrisumlem2  25079  dchrisumlem3  25080  chirred  29103  iundisjf  29247  fmptcof2  29299  esumfsup  29913  esum2d  29936  measvunilem  30056  measvunilem0  30057  phpreu  33025  poimirlem26  33067  poimirlem27  33068  poimirlem28  33069  itggt0cn  33114  ftc1anclem5  33121  cdleme26ee  35128  cdlemefs32sn1aw  35182  cdleme41sn3a  35201  cdleme32d  35212  cdleme32f  35214  cdlemk38  35683  cdlemk11t  35714  monotoddzz  36988  oddcomabszz  36989  evth2f  38657  evthf  38669  rfcnpre3  38675  rfcnpre4  38676  rfcnnnub  38678  ssfiunibd  38987  uzub  39122  fsumlessf  39213  fmul01  39216  fmul01lt1lem1  39220  fmul01lt1  39222  climinff  39247  idlimc  39262  limcperiod  39264  fnlimabslt  39315  limsupref  39321  limsupbnd1f  39322  climbddf  39323  limsuppnfd  39338  climinf2  39343  limsuppnf  39347  limsupubuz  39349  climinf2mpt  39350  climinfmpt  39351  limsupmnf  39357  limsupre2  39361  limsupmnfuz  39363  limsupre3  39369  limsupre3uz  39372  limsupreuz  39373  cncfshift  39390  cncficcgt0  39405  stoweidlem3  39527  stoweidlem26  39550  stoweidlem28  39552  stoweidlem31  39555  stoweidlem51  39575  stoweidlem52  39576  stoweidlem59  39583  stirling  39613  fourierdlem20  39651  fourierdlem79  39709  etransclem48  39806  sge0ltfirp  39924  sge0lempt  39934  iunhoiioolem  40196  pimltmnf2  40218  pimgtpnf2  40224  pimltpnf2  40230  pimgtmnf2  40231  pimdecfgtioc  40232  issmff  40250  smfpimltxrmpt  40274  smfpreimagtf  40283  smflim  40292  smfpimgtxr  40295  smfpimgtxrmpt  40299  smfsup  40327  smfinflem  40330  smfinf  40331  prmdvdsfmtnof1lem1  40795  dffun3f  41721  setrec2  41735
  Copyright terms: Public domain W3C validator