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

Theorem nfbr 4851
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 4850 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87trud 1642 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1633  wnf 1857  wnfc 2889   class class class wbr 4804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805
This theorem is referenced by:  sbcbr123  4858  nfpo  5192  nfso  5193  pofun  5203  nffr  5240  nfse  5241  nfco  5443  nfcnv  5456  dfdmf  5472  dfrnf  5519  nfdm  5522  dfrel4  5743  dffun6f  6063  nffv  6359  funfv2f  6429  fvopab5  6472  f1ompt  6545  fmptco  6559  nfiso  6735  ofrfval2  7080  tposoprab  7557  xpcomco  8215  nfoi  8584  tskwe  8966  cardmin2  9014  uniimadomf  9559  cardmin  9578  inar1  9789  lble  11167  rlim2  14426  ello1mpt  14451  rlimcld2  14508  o1compt  14517  nfsum1  14619  nfsum  14620  fsum00  14729  fsumrlim  14742  o1fsum  14744  nfcprod1  14839  nfcprod  14840  sumeven  15312  sumodd  15313  invfuc  16835  dprd2d2  18643  2ndcdisj  21461  ovoliunlem3  23472  mbfpos  23617  mbfposb  23619  mbfsup  23630  mbfinf  23631  i1fposd  23673  itg2splitlem  23714  itg2split  23715  isibl2  23732  nfitg  23740  cbvitg  23741  itggt0  23807  dvlipcn  23956  dvfsumle  23983  dvfsumabs  23985  dvfsumlem2  23989  dvfsumlem4  23991  dvfsumrlim  23993  dvfsum2  23996  rlimcnp  24891  lgamgulmlem2  24955  lgamgulmlem6  24959  dchrisumlema  25376  dchrisumlem2  25378  dchrisumlem3  25379  chirred  29563  iundisjf  29709  fmptcof2  29766  fsumiunle  29884  esumfsup  30441  esum2d  30464  measvunilem  30584  measvunilem0  30585  nosupbnd1  32166  nosupbnd2  32168  phpreu  33706  poimirlem26  33748  poimirlem27  33749  poimirlem28  33750  itggt0cn  33795  ftc1anclem5  33802  cdleme26ee  36150  cdlemefs32sn1aw  36204  cdleme41sn3a  36223  cdleme32d  36234  cdleme32f  36236  cdlemk38  36705  cdlemk11t  36736  monotoddzz  38010  oddcomabszz  38011  evth2f  39673  evthf  39685  rfcnpre3  39691  rfcnpre4  39692  rfcnnnub  39694  ssfiunibd  40022  uzub  40156  supxrleubrnmptf  40178  infrpgernmpt  40193  monoordxr  40211  monoord2xr  40213  fsumlessf  40312  fmul01  40315  fmul01lt1lem1  40319  fmul01lt1  40321  climinff  40346  idlimc  40361  limcperiod  40363  fnlimabslt  40414  limsupref  40420  limsupbnd1f  40421  climbddf  40422  limsuppnfd  40437  climinf2  40442  limsuppnf  40446  limsupubuz  40448  climinf2mpt  40449  climinfmpt  40450  limsupmnf  40456  limsupre2  40460  limsupmnfuz  40462  limsupre3  40468  limsupre3uz  40471  limsupreuz  40472  climuz  40479  limsupgt  40513  liminfreuz  40538  liminflt  40540  xlimmnf  40570  xlimpnf  40571  dfxlim2  40577  cncfshift  40590  cncficcgt0  40604  stoweidlem3  40723  stoweidlem26  40746  stoweidlem28  40748  stoweidlem31  40751  stoweidlem51  40771  stoweidlem52  40772  stoweidlem59  40779  stirling  40809  fourierdlem20  40847  fourierdlem79  40905  etransclem48  41002  sge0ltfirp  41120  sge0lempt  41130  meaiunincf  41203  iunhoiioolem  41395  pimltmnf2  41417  pimgtpnf2  41423  pimltpnf2  41429  pimgtmnf2  41430  pimdecfgtioc  41431  issmff  41449  smfpimltxrmpt  41473  smfpreimagtf  41482  smflim  41491  smfpimgtxr  41494  smfpimgtxrmpt  41498  smfsup  41526  smfinflem  41529  smfinf  41530  prmdvdsfmtnof1lem1  42006  dffun3f  42939  setrec2  42952
  Copyright terms: Public domain W3C validator