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

Theorem nfbr 4067
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 4066 . 2  |-  (  T. 
->  F/ x  A R B )
87trud 1314 1  |-  F/ x  A R B
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1531   F/_wnfc 2406   class class class wbr 4023
This theorem is referenced by:  sbcbrg  4072  nfpo  4319  nfso  4320  pofun  4330  nffr  4367  nfse  4368  nfco  4849  nfcnv  4860  dfdmf  4873  dfrnf  4917  nfdm  4920  dffun6f  5269  nffv  5532  funfv2f  5588  f1ompt  5682  fmptco  5691  nfiso  5821  nfofr  6084  ofrfval2  6096  tposoprab  6270  fvopab5  6289  xpcomco  6952  nfoi  7229  tskwe  7583  cardmin2  7631  axdclem  8146  uniimadomf  8167  cardmin  8186  inar1  8397  lble  9706  rlim2  11970  ello1mpt  11995  rlimcld2  12052  o1compt  12061  nfsum1  12163  nfsum  12164  fsum00  12256  fsumrlim  12269  o1fsum  12271  invfuc  13848  dprd2d2  15279  2ndcdisj  17182  ovoliunlem3  18863  mbfpos  19006  mbfposb  19008  mbfsup  19019  mbfinf  19020  i1fposd  19062  itg2splitlem  19103  itg2split  19104  isibl2  19121  nfitg  19129  cbvitg  19130  itggt0  19196  dvlipcn  19341  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  rlimcnp  20260  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  chirred  22975  dfrel4  23204  fmptcof2  23229  iundisjf  23365  measvunilem  23540  measvunilem0  23541  monotoddzz  27028  oddcomabszz  27029  evth2f  27686  evthf  27698  rfcnpre3  27704  rfcnpre4  27705  rfcnnnub  27707  fmul01  27710  fmul01lt1lem1  27714  fmul01lt1  27716  climinff  27737  stoweidlem3  27752  stoweidlem26  27775  stoweidlem28  27777  stoweidlem31  27780  stoweidlem51  27800  stoweidlem52  27801  stoweidlem59  27808  stirling  27838  cdleme26ee  30549  cdlemefs32sn1aw  30603  cdleme41sn3a  30622  cdleme32d  30633  cdleme32f  30635  cdlemk38  31104  cdlemk11t  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator