![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfbr | 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 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | nfbr.2 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | nfbr.3 |
. . . 4
![]() ![]() ![]() ![]() | |
6 | 5 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 4, 6 | nfbrd 4050 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | mptru 1362 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-un 3135 df-sn 3600 df-pr 3601 df-op 3603 df-br 4006 |
This theorem is referenced by: sbcbrg 4059 nfpo 4303 nfso 4304 pofun 4314 nfse 4343 nffrfor 4350 nfwe 4357 nfco 4794 nfcnv 4808 dfdmf 4822 dfrnf 4870 nfdm 4873 dffun6f 5231 dffun4f 5234 nffv 5527 funfvdm2f 5584 fvmptss2 5594 f1ompt 5670 fmptco 5685 nfiso 5810 nfofr 6092 ofrfval2 6102 tposoprab 6284 xpcomco 6829 nfsup 6994 caucvgprprlemaddq 7710 lble 8907 nfsum1 11367 nfsum 11368 fsum00 11473 mertenslem2 11547 nfcprod1 11565 nfcprod 11566 fprodap0 11632 fprodrec 11640 fproddivapf 11642 fprodap0f 11647 fprodle 11651 oddpwdclemdvds 12173 oddpwdclemndvds 12174 |
Copyright terms: Public domain | W3C validator |