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

Theorem nfbr 4148
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  |-  F/_ x A
nfbr.2  |-  F/_ x R
nfbr.3  |-  F/_ x B
Assertion
Ref Expression
nfbr  |-  F/ x  A R B

Proof of Theorem nfbr
StepHypRef Expression
1 nfbr.1 . . . 4  |-  F/_ x A
21a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
3 nfbr.2 . . . 4  |-  F/_ x R
43a1i 10 . . 3  |-  (  T. 
->  F/_ x R )
5 nfbr.3 . . . 4  |-  F/_ x B
65a1i 10 . . 3  |-  (  T. 
->  F/_ x B )
72, 4, 6nfbrd 4147 . 2  |-  (  T. 
->  F/ x  A R B )
87trud 1323 1  |-  F/ x  A R B
Colors of variables: wff set class
Syntax hints:    T. wtru 1316   F/wnf 1544   F/_wnfc 2481   class class class wbr 4104
This theorem is referenced by:  sbcbrg  4153  nfpo  4401  nfso  4402  pofun  4412  nffr  4449  nfse  4450  nfco  4931  nfcnv  4942  dfdmf  4955  dfrnf  4999  nfdm  5002  dffun6f  5351  nffv  5615  funfv2f  5671  f1ompt  5765  fmptco  5774  nfiso  5908  nfofr  6171  ofrfval2  6183  tposoprab  6357  fvopab5  6376  xpcomco  7040  nfoi  7319  tskwe  7673  cardmin2  7721  axdclem  8236  uniimadomf  8257  cardmin  8276  inar1  8487  lble  9796  rlim2  12066  ello1mpt  12091  rlimcld2  12148  o1compt  12157  nfsum1  12260  nfsum  12261  fsum00  12353  fsumrlim  12366  o1fsum  12368  invfuc  13947  dprd2d2  15378  2ndcdisj  17288  ovoliunlem3  18967  mbfpos  19110  mbfposb  19112  mbfsup  19123  mbfinf  19124  i1fposd  19166  itg2splitlem  19207  itg2split  19208  isibl2  19225  nfitg  19233  cbvitg  19234  itggt0  19300  dvlipcn  19445  dvfsumle  19472  dvfsumabs  19474  dvfsumlem2  19478  dvfsumlem4  19480  dvfsumrlim  19482  dvfsum2  19485  rlimcnp  20371  dchrisumlema  20749  dchrisumlem2  20751  dchrisumlem3  20752  chirred  23089  iundisjf  23227  dfrel4  23242  fmptcof2  23280  esumfsup  23726  measvunilem  23830  measvunilem0  23831  lgamgulmlem2  24063  lgamgulmlem6  24067  nfcprod1  24537  nfcprod  24538  itggt0cn  25512  monotoddzz  26351  oddcomabszz  26352  evth2f  27009  evthf  27021  rfcnpre3  27027  rfcnpre4  27028  rfcnnnub  27030  fmul01  27033  fmul01lt1lem1  27037  fmul01lt1  27039  climinff  27060  stoweidlem3  27075  stoweidlem26  27098  stoweidlem28  27100  stoweidlem31  27103  stoweidlem51  27123  stoweidlem52  27124  stoweidlem59  27131  stirling  27161  cdleme26ee  30618  cdlemefs32sn1aw  30672  cdleme41sn3a  30691  cdleme32d  30702  cdleme32f  30704  cdlemk38  31173  cdlemk11t  31204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105
  Copyright terms: Public domain W3C validator