Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfbr | GIF 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 3981 | . 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵) |
8 | 7 | mptru 1341 | 1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵 |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1333 Ⅎwnf 1437 Ⅎwnfc 2269 class class class wbr 3937 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-un 3080 df-sn 3538 df-pr 3539 df-op 3541 df-br 3938 |
This theorem is referenced by: sbcbrg 3990 nfpo 4231 nfso 4232 pofun 4242 nfse 4271 nffrfor 4278 nfwe 4285 nfco 4712 nfcnv 4726 dfdmf 4740 dfrnf 4788 nfdm 4791 dffun6f 5144 dffun4f 5147 nffv 5439 funfvdm2f 5494 fvmptss2 5504 f1ompt 5579 fmptco 5594 nfiso 5715 nfofr 5996 ofrfval2 6006 tposoprab 6185 xpcomco 6728 nfsup 6887 caucvgprprlemaddq 7540 lble 8729 nfsum1 11157 nfsum 11158 fsum00 11263 mertenslem2 11337 nfcprod1 11355 nfcprod 11356 oddpwdclemdvds 11884 oddpwdclemndvds 11885 |
Copyright terms: Public domain | W3C validator |