![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > r19.41v | Unicode version |
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.) |
Ref | Expression |
---|---|
r19.41v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1466 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | r19.41 2522 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 df-nf 1395 df-rex 2365 |
This theorem is referenced by: r19.42v 2524 3reeanv 2537 reuind 2820 iuncom4 3735 dfiun2g 3760 iunxiun 3808 inuni 3989 xpiundi 4492 xpiundir 4493 imaco 4931 coiun 4935 abrexco 5530 imaiun 5531 isoini 5589 rexrnmpt2 5752 mapsnen 6518 genpassl 7073 genpassu 7074 4fvwrd4 9539 |
Copyright terms: Public domain | W3C validator |