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

Theorem nfbr 4248
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 11 . . 3  |-  (  T. 
->  F/_ x A )
3 nfbr.2 . . . 4  |-  F/_ x R
43a1i 11 . . 3  |-  (  T. 
->  F/_ x R )
5 nfbr.3 . . . 4  |-  F/_ x B
65a1i 11 . . 3  |-  (  T. 
->  F/_ x B )
72, 4, 6nfbrd 4247 . 2  |-  (  T. 
->  F/ x  A R B )
87trud 1332 1  |-  F/ x  A R B
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/wnf 1553   F/_wnfc 2558   class class class wbr 4204
This theorem is referenced by:  sbcbrg  4253  nfpo  4500  nfso  4501  pofun  4511  nffr  4548  nfse  4549  nfco  5029  nfcnv  5042  dfdmf  5055  dfrnf  5099  nfdm  5102  dffun6f  5459  nffv  5726  funfv2f  5783  f1ompt  5882  fmptco  5892  nfiso  6035  ofrfval2  6314  tposoprab  6506  fvopab5  6525  xpcomco  7189  nfoi  7472  tskwe  7826  cardmin2  7874  uniimadomf  8409  cardmin  8428  inar1  8639  lble  9949  rlim2  12278  ello1mpt  12303  rlimcld2  12360  o1compt  12369  nfsum1  12472  nfsum  12473  fsum00  12565  fsumrlim  12578  o1fsum  12580  invfuc  14159  dprd2d2  15590  2ndcdisj  17507  ovoliunlem3  19388  mbfpos  19531  mbfposb  19533  mbfsup  19544  mbfinf  19545  i1fposd  19587  itg2splitlem  19628  itg2split  19629  isibl2  19646  nfitg  19654  cbvitg  19655  itggt0  19721  dvlipcn  19866  dvfsumle  19893  dvfsumabs  19895  dvfsumlem2  19899  dvfsumlem4  19901  dvfsumrlim  19903  dvfsum2  19906  rlimcnp  20792  dchrisumlema  21170  dchrisumlem2  21172  dchrisumlem3  21173  chirred  23886  iundisjf  24017  dfrel4  24022  fmptcof2  24064  esumfsup  24448  measvunilem  24554  measvunilem0  24555  lgamgulmlem2  24802  lgamgulmlem6  24806  nfcprod1  25225  nfcprod  25226  itggt0cn  26223  monotoddzz  26943  oddcomabszz  26944  evth2f  27600  evthf  27612  rfcnpre3  27618  rfcnpre4  27619  rfcnnnub  27621  fmul01  27624  fmul01lt1lem1  27628  fmul01lt1  27630  climinff  27651  stoweidlem3  27666  stoweidlem26  27689  stoweidlem28  27691  stoweidlem31  27694  stoweidlem51  27714  stoweidlem52  27715  stoweidlem59  27722  stirling  27752  cdleme26ee  30996  cdlemefs32sn1aw  31050  cdleme41sn3a  31069  cdleme32d  31080  cdleme32f  31082  cdlemk38  31551  cdlemk11t  31582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator