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

Theorem nfbr 5109
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 5108 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87mptru 1550 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1544  wnf 1791  wnfc 2885   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-rab 3071  df-v 3417  df-dif 3878  df-un 3880  df-nul 4247  df-if 4449  df-sn 4551  df-pr 4553  df-op 4557  df-br 5063
This theorem is referenced by:  sbcbr123  5116  nfpo  5482  nfso  5483  pofun  5495  nffr  5534  nfse  5535  nfco  5743  nfcnv  5756  dfdmf  5774  dfrnf  5828  nfdm  5829  dfrel4  6063  dffun6f  6403  nffv  6736  funfv2f  6809  fvopab5  6859  f1ompt  6937  fmptco  6953  nfiso  7140  nfofr  7484  ofrfval2  7498  tposoprab  8013  xpcomco  8746  nfoi  9143  tskwe  9579  cardmin2  9628  uniimadomf  10172  cardmin  10191  inar1  10402  lble  11797  rlim2  15070  ello1mpt  15095  rlimcld2  15152  o1compt  15161  nfsum1  15266  nfsum  15267  nfsumOLD  15268  fsum00  15375  fsumrlim  15388  o1fsum  15390  nfcprod1  15485  nfcprod  15486  sumeven  15961  sumodd  15962  invfuc  17496  dprd2d2  19444  2ndcdisj  22366  ovoliunlem3  24414  mbfpos  24561  mbfposb  24563  mbfsup  24574  mbfinf  24575  i1fposd  24618  itg2splitlem  24659  itg2split  24660  isibl2  24677  nfitg  24685  cbvitg  24686  itggt0  24754  dvlipcn  24904  dvfsumle  24931  dvfsumabs  24933  dvfsumlem2  24937  dvfsumlem4  24939  dvfsumrlim  24941  dvfsum2  24944  rlimcnp  25861  lgamgulmlem2  25925  lgamgulmlem6  25929  dchrisumlema  26382  dchrisumlem2  26384  dchrisumlem3  26385  chirred  30489  iundisjf  30660  fmptcof2  30727  fsumiunle  30876  esumfsup  31763  esum2d  31786  measvunilem  31905  measvunilem0  31906  nosupbnd1  33667  nosupbnd2  33669  noinfbnd1  33682  noinfbnd2  33684  bj-opabco  35107  phpreu  35511  poimirlem26  35553  poimirlem27  35554  poimirlem28  35555  itggt0cn  35597  ftc1anclem5  35604  cdleme26ee  38124  cdlemefs32sn1aw  38178  cdleme41sn3a  38197  cdleme32d  38208  cdleme32f  38210  cdlemk38  38679  cdlemk11t  38710  monotoddzz  40483  oddcomabszz  40484  evth2f  42246  evthf  42258  rfcnpre3  42264  rfcnpre4  42265  rfcnnnub  42267  ssfiunibd  42536  uzub  42659  supxrleubrnmptf  42681  infrpgernmpt  42695  monoordxr  42713  monoord2xr  42715  fsumlessf  42808  fmul01  42811  fmul01lt1lem1  42815  fmul01lt1  42817  climinff  42842  idlimc  42857  limcperiod  42859  fnlimabslt  42910  limsupref  42916  limsupbnd1f  42917  climbddf  42918  limsuppnfd  42933  climinf2  42938  limsuppnf  42942  limsupubuz  42944  climinf2mpt  42945  climinfmpt  42946  limsupmnf  42952  limsupre2  42956  limsupmnfuz  42958  limsupre3  42964  limsupre3uz  42967  limsupreuz  42968  climuz  42975  limsupgt  43009  liminfreuz  43034  liminflt  43036  xlimpnfxnegmnf  43045  xlimmnf  43072  xlimpnf  43073  dfxlim2  43079  cncfshift  43105  cncficcgt0  43119  stoweidlem3  43234  stoweidlem26  43257  stoweidlem28  43259  stoweidlem31  43262  stoweidlem51  43282  stoweidlem52  43283  stoweidlem59  43290  stirling  43320  fourierdlem20  43358  fourierdlem79  43416  etransclem48  43513  sge0ltfirp  43628  sge0lempt  43638  meaiunincf  43711  iunhoiioolem  43903  pimltmnf2  43925  pimgtpnf2  43931  pimltpnf2  43937  pimgtmnf2  43938  pimdecfgtioc  43939  issmff  43957  smfpimltxrmpt  43981  smfpreimagtf  43990  smflim  43999  smfpimgtxr  44002  smfpimgtxrmpt  44006  smfsup  44034  smfinflem  44037  smfinf  44038  nfafv2  44397  prmdvdsfmtnof1lem1  44724  dffun3f  46074  setrec2  46087
  Copyright terms: Public domain W3C validator