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

Theorem nfbr 4669
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 4668 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87trud 1490 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnf 1705  wnfc 2748   class class class wbr 4623
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 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624
This theorem is referenced by:  sbcbr123  4676  nfpo  5010  nfso  5011  pofun  5021  nffr  5058  nfse  5059  nfco  5257  nfcnv  5271  dfdmf  5287  dfrnf  5334  nfdm  5337  dfrel4  5554  dffun6f  5871  nffv  6165  funfv2f  6234  fvopab5  6275  f1ompt  6348  fmptco  6362  nfiso  6537  ofrfval2  6880  tposoprab  7348  xpcomco  8010  nfoi  8379  tskwe  8736  cardmin2  8784  uniimadomf  9327  cardmin  9346  inar1  9557  lble  10935  rlim2  14177  ello1mpt  14202  rlimcld2  14259  o1compt  14268  nfsum1  14370  nfsum  14371  fsum00  14476  fsumrlim  14489  o1fsum  14491  nfcprod1  14584  nfcprod  14585  sumeven  15053  sumodd  15054  invfuc  16574  dprd2d2  18383  2ndcdisj  21199  ovoliunlem3  23212  mbfpos  23358  mbfposb  23360  mbfsup  23371  mbfinf  23372  i1fposd  23414  itg2splitlem  23455  itg2split  23456  isibl2  23473  nfitg  23481  cbvitg  23482  itggt0  23548  dvlipcn  23695  dvfsumle  23722  dvfsumabs  23724  dvfsumlem2  23728  dvfsumlem4  23730  dvfsumrlim  23732  dvfsum2  23735  rlimcnp  24626  lgamgulmlem2  24690  lgamgulmlem6  24694  dchrisumlema  25111  dchrisumlem2  25113  dchrisumlem3  25114  chirred  29142  iundisjf  29288  fmptcof2  29340  esumfsup  29955  esum2d  29978  measvunilem  30098  measvunilem0  30099  phpreu  33064  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  itggt0cn  33153  ftc1anclem5  33160  cdleme26ee  35167  cdlemefs32sn1aw  35221  cdleme41sn3a  35240  cdleme32d  35251  cdleme32f  35253  cdlemk38  35722  cdlemk11t  35753  monotoddzz  37027  oddcomabszz  37028  evth2f  38696  evthf  38708  rfcnpre3  38714  rfcnpre4  38715  rfcnnnub  38717  ssfiunibd  39022  uzub  39157  fsumlessf  39245  fmul01  39248  fmul01lt1lem1  39252  fmul01lt1  39254  climinff  39279  idlimc  39294  limcperiod  39296  fnlimabslt  39347  limsupref  39353  limsupbnd1f  39354  climbddf  39355  limsuppnfd  39370  climinf2  39375  limsuppnf  39379  limsupubuz  39381  climinf2mpt  39382  climinfmpt  39383  limsupmnf  39389  limsupre2  39393  limsupmnfuz  39395  limsupre3  39401  limsupre3uz  39404  limsupreuz  39405  cncfshift  39422  cncficcgt0  39436  stoweidlem3  39557  stoweidlem26  39580  stoweidlem28  39582  stoweidlem31  39585  stoweidlem51  39605  stoweidlem52  39606  stoweidlem59  39613  stirling  39643  fourierdlem20  39681  fourierdlem79  39739  etransclem48  39836  sge0ltfirp  39954  sge0lempt  39964  iunhoiioolem  40226  pimltmnf2  40248  pimgtpnf2  40254  pimltpnf2  40260  pimgtmnf2  40261  pimdecfgtioc  40262  issmff  40280  smfpimltxrmpt  40304  smfpreimagtf  40313  smflim  40322  smfpimgtxr  40325  smfpimgtxrmpt  40329  smfsup  40357  smfinflem  40360  smfinf  40361  prmdvdsfmtnof1lem1  40825  dffun3f  41751  setrec2  41765
  Copyright terms: Public domain W3C validator