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

Theorem nfbr 5106
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 5105 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87mptru 1540 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1534  wnf 1780  wnfc 2961   class class class wbr 5059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060
This theorem is referenced by:  sbcbr123  5113  nfpo  5474  nfso  5475  pofun  5486  nffr  5524  nfse  5525  nfco  5731  nfcnv  5744  dfdmf  5760  dfrnf  5815  nfdm  5818  dfrel4  6043  dffun6f  6364  nffv  6675  funfv2f  6747  fvopab5  6795  f1ompt  6870  fmptco  6886  nfiso  7069  nfofr  7409  ofrfval2  7421  tposoprab  7922  xpcomco  8601  nfoi  8972  tskwe  9373  cardmin2  9421  uniimadomf  9961  cardmin  9980  inar1  10191  lble  11587  rlim2  14847  ello1mpt  14872  rlimcld2  14929  o1compt  14938  nfsum1  15040  nfsumw  15041  nfsum  15042  fsum00  15147  fsumrlim  15160  o1fsum  15162  nfcprod1  15258  nfcprod  15259  sumeven  15732  sumodd  15733  invfuc  17238  dprd2d2  19160  2ndcdisj  22058  ovoliunlem3  24099  mbfpos  24246  mbfposb  24248  mbfsup  24259  mbfinf  24260  i1fposd  24302  itg2splitlem  24343  itg2split  24344  isibl2  24361  nfitg  24369  cbvitg  24370  itggt0  24436  dvlipcn  24585  dvfsumle  24612  dvfsumabs  24614  dvfsumlem2  24618  dvfsumlem4  24620  dvfsumrlim  24622  dvfsum2  24625  rlimcnp  25537  lgamgulmlem2  25601  lgamgulmlem6  25605  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  chirred  30166  iundisjf  30333  fmptcof2  30396  fsumiunle  30540  esumfsup  31324  esum2d  31347  measvunilem  31466  measvunilem0  31467  nosupbnd1  33209  nosupbnd2  33211  phpreu  34870  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  itggt0cn  34958  ftc1anclem5  34965  cdleme26ee  37490  cdlemefs32sn1aw  37544  cdleme41sn3a  37563  cdleme32d  37574  cdleme32f  37576  cdlemk38  38045  cdlemk11t  38076  monotoddzz  39533  oddcomabszz  39534  evth2f  41265  evthf  41277  rfcnpre3  41283  rfcnpre4  41284  rfcnnnub  41286  ssfiunibd  41568  uzub  41697  supxrleubrnmptf  41719  infrpgernmpt  41733  monoordxr  41751  monoord2xr  41753  fsumlessf  41850  fmul01  41853  fmul01lt1lem1  41857  fmul01lt1  41859  climinff  41884  idlimc  41899  limcperiod  41901  fnlimabslt  41952  limsupref  41958  limsupbnd1f  41959  climbddf  41960  limsuppnfd  41975  climinf2  41980  limsuppnf  41984  limsupubuz  41986  climinf2mpt  41987  climinfmpt  41988  limsupmnf  41994  limsupre2  41998  limsupmnfuz  42000  limsupre3  42006  limsupre3uz  42009  limsupreuz  42010  climuz  42017  limsupgt  42051  liminfreuz  42076  liminflt  42078  xlimpnfxnegmnf  42087  xlimmnf  42114  xlimpnf  42115  dfxlim2  42121  cncfshift  42149  cncficcgt0  42163  stoweidlem3  42281  stoweidlem26  42304  stoweidlem28  42306  stoweidlem31  42309  stoweidlem51  42329  stoweidlem52  42330  stoweidlem59  42337  stirling  42367  fourierdlem20  42405  fourierdlem79  42463  etransclem48  42560  sge0ltfirp  42675  sge0lempt  42685  meaiunincf  42758  iunhoiioolem  42950  pimltmnf2  42972  pimgtpnf2  42978  pimltpnf2  42984  pimgtmnf2  42985  pimdecfgtioc  42986  issmff  43004  smfpimltxrmpt  43028  smfpreimagtf  43037  smflim  43046  smfpimgtxr  43049  smfpimgtxrmpt  43053  smfsup  43081  smfinflem  43084  smfinf  43085  nfafv2  43410  prmdvdsfmtnof1lem1  43739  dffun3f  44778  setrec2  44791
  Copyright terms: Public domain W3C validator