![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfbr | Structured version Visualization version Unicode version |
Description: Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
nfbr.1 |
![]() ![]() ![]() ![]() |
nfbr.2 |
![]() ![]() ![]() ![]() |
nfbr.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfbr |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfbr.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | nfbr.2 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | nfbr.3 |
. . . 4
![]() ![]() ![]() ![]() | |
6 | 5 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 4, 6 | nfbrd 4446 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | trud 1453 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 |
This theorem is referenced by: sbcbr123 4454 nfpo 4760 nfso 4761 pofun 4771 nffr 4808 nfse 4809 nfco 5000 nfcnv 5013 dfdmf 5028 dfrnf 5073 nfdm 5076 dffun6f 5596 nffv 5872 funfv2f 5934 fvopab5 5974 f1ompt 6044 fmptco 6056 nfiso 6215 ofrfval2 6549 tposoprab 7009 xpcomco 7662 nfoi 8029 tskwe 8384 cardmin2 8432 uniimadomf 8970 cardmin 8989 inar1 9200 lble 10558 rlim2 13560 ello1mpt 13585 rlimcld2 13642 o1compt 13651 nfsum1 13756 nfsum 13757 fsum00 13858 fsumrlim 13871 o1fsum 13873 nfcprod1 13964 nfcprod 13965 invfuc 15879 dprd2d2 17677 2ndcdisj 20471 ovoliunlem3 22457 mbfpos 22607 mbfposb 22609 mbfsup 22620 mbfinf 22621 mbfinfOLD 22622 i1fposd 22665 itg2splitlem 22706 itg2split 22707 isibl2 22724 nfitg 22732 cbvitg 22733 itggt0 22799 dvlipcn 22946 dvfsumle 22973 dvfsumabs 22975 dvfsumlem2 22979 dvfsumlem4 22981 dvfsumrlim 22983 dvfsum2 22986 rlimcnp 23891 lgamgulmlem2 23955 lgamgulmlem6 23959 dchrisumlema 24326 dchrisumlem2 24328 dchrisumlem3 24329 chirred 28048 iundisjf 28199 dfrel4 28208 fmptcof2 28259 esumfsup 28891 esum2d 28914 measvunilem 29034 measvunilem0 29035 phpreu 31929 poimirlem26 31966 poimirlem27 31967 poimirlem28 31968 itggt0cn 32014 ftc1anclem5 32021 cdleme26ee 33927 cdlemefs32sn1aw 33981 cdleme41sn3a 34000 cdleme32d 34011 cdleme32f 34013 cdlemk38 34482 cdlemk11t 34513 monotoddzz 35791 oddcomabszz 35792 evth2f 37336 evthf 37348 rfcnpre3 37354 rfcnpre4 37355 rfcnnnub 37357 ssfiunibd 37527 fsumlessf 37656 fmul01 37658 fmul01lt1lem1 37662 fmul01lt1 37664 climinff 37690 climinffOLD 37691 idlimc 37706 limcperiod 37708 cncfshift 37751 cncficcgt0 37766 stoweidlem3 37863 stoweidlem26 37886 stoweidlem28 37888 stoweidlem31 37892 stoweidlem51 37912 stoweidlem52 37913 stoweidlem59 37920 stirling 37951 fourierdlem20 37989 fourierdlem79 38049 etransclem48OLD 38147 etransclem48 38148 sge0ltfirp 38242 sge0lempt 38252 |
Copyright terms: Public domain | W3C validator |