![]() |
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 1489 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | r19.41 2558 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-17 1487 ax-ial 1495 |
This theorem depends on definitions: df-bi 116 df-nf 1418 df-rex 2394 |
This theorem is referenced by: r19.42v 2560 3reeanv 2573 reuind 2856 iuncom4 3784 dfiun2g 3809 iunxiun 3858 inuni 4038 xpiundi 4555 xpiundir 4556 imaco 5000 coiun 5004 abrexco 5612 imaiun 5613 isoini 5671 rexrnmpo 5838 mapsnen 6657 genpassl 7274 genpassu 7275 4fvwrd4 9804 metrest 12489 |
Copyright terms: Public domain | W3C validator |