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 4009 | . 2 |
8 | 7 | mptru 1344 | 1 |
Colors of variables: wff set class |
Syntax hints: wtru 1336 wnf 1440 wnfc 2286 class class class wbr 3965 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 df-un 3106 df-sn 3566 df-pr 3567 df-op 3569 df-br 3966 |
This theorem is referenced by: sbcbrg 4018 nfpo 4261 nfso 4262 pofun 4272 nfse 4301 nffrfor 4308 nfwe 4315 nfco 4750 nfcnv 4764 dfdmf 4778 dfrnf 4826 nfdm 4829 dffun6f 5182 dffun4f 5185 nffv 5477 funfvdm2f 5532 fvmptss2 5542 f1ompt 5617 fmptco 5632 nfiso 5753 nfofr 6035 ofrfval2 6045 tposoprab 6224 xpcomco 6768 nfsup 6933 caucvgprprlemaddq 7623 lble 8813 nfsum1 11248 nfsum 11249 fsum00 11354 mertenslem2 11428 nfcprod1 11446 nfcprod 11447 fprodap0 11513 fprodrec 11521 fproddivapf 11523 fprodap0f 11528 fprodle 11532 oddpwdclemdvds 12039 oddpwdclemndvds 12040 |
Copyright terms: Public domain | W3C validator |