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

Theorem nfbr 4069
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 12 . . 3  |-  (  T. 
->  F/_ x A )
3 nfbr.2 . . . 4  |-  F/_ x R
43a1i 12 . . 3  |-  (  T. 
->  F/_ x R )
5 nfbr.3 . . . 4  |-  F/_ x B
65a1i 12 . . 3  |-  (  T. 
->  F/_ x B )
72, 4, 6nfbrd 4068 . 2  |-  (  T. 
->  F/ x  A R B )
87trud 1316 1  |-  F/ x  A R B
Colors of variables: wff set class
Syntax hints:    T. wtru 1309   F/wnf 1532   F/_wnfc 2408   class class class wbr 4025
This theorem is referenced by:  sbcbrg  4074  nfpo  4319  nfso  4320  pofun  4330  nffr  4367  nfse  4368  nfco  4849  nfcnv  4860  dfdmf  4873  dfrnf  4917  nfdm  4920  dffun6f  5236  funfv2f  5550  f1ompt  5644  fmptco  5653  nfiso  5783  nfofr  6046  ofrfval2  6058  tposoprab  6232  fvopab5  6283  xpcomco  6948  nfoi  7225  tskwe  7579  cardmin2  7627  axdclem  8142  uniimadomf  8163  cardmin  8182  inar1  8393  lble  9702  rlim2  11965  ello1mpt  11990  rlimcld2  12047  o1compt  12056  nfsum1  12158  nfsum  12159  fsum00  12251  fsumrlim  12264  o1fsum  12266  invfuc  13843  dprd2d2  15274  2ndcdisj  17177  ovoliunlem3  18858  mbfpos  19001  mbfposb  19003  mbfsup  19014  mbfinf  19015  i1fposd  19057  itg2splitlem  19098  itg2split  19099  isibl2  19116  nfitg  19124  cbvitg  19125  itggt0  19191  dvlipcn  19336  dvfsumle  19363  dvfsumabs  19365  dvfsumlem2  19369  dvfsumlem4  19371  dvfsumrlim  19373  dvfsum2  19376  rlimcnp  20255  dchrisumlema  20632  dchrisumlem2  20634  dchrisumlem3  20635  chirred  22968  monotoddzz  26428  oddcomabszz  26429  evth2f  27086  evthf  27098  rfcnpre3  27104  rfcnpre4  27105  rfcnnnub  27107  fmul01  27110  fmul01lt1lem1  27114  fmul01lt1  27116  climinff  27137  stoweidlem3  27152  stoweidlem26  27175  stoweidlem28  27177  stoweidlem31  27180  stoweidlem51  27200  stoweidlem52  27201  stoweidlem59  27208  stirling  27238  cdleme26ee  29817  cdlemefs32sn1aw  29871  cdleme41sn3a  29890  cdleme32d  29901  cdleme32f  29903  cdlemk38  30372  cdlemk11t  30403
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator