Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimiv | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
ralrimiv.1 |
Ref | Expression |
---|---|
ralrimiv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1493 | . 2 | |
2 | ralrimiv.1 | . 2 | |
3 | 1, 2 | ralrimi 2480 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 wral 2393 |
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-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 |
This theorem is referenced by: ralrimiva 2482 ralrimivw 2483 ralrimivv 2490 r19.27av 2544 rr19.3v 2797 rabssdv 3147 rzal 3430 trin 4006 class2seteq 4057 ralxfrALT 4358 ssorduni 4373 ordsucim 4386 onintonm 4403 issref 4891 funimaexglem 5176 resflem 5552 poxp 6097 rdgss 6248 dom2lem 6634 supisoti 6865 ordiso2 6888 updjud 6935 uzind 9130 zindd 9137 lbzbi 9376 icoshftf1o 9742 maxabslemval 10948 xrmaxiflemval 10987 fisum0diag2 11184 alzdvds 11479 hashgcdeq 11831 tgcl 12160 distop 12181 neiuni 12257 cnpnei 12315 isxmetd 12443 fsumcncntop 12652 bj-nntrans2 13077 bj-inf2vnlem1 13095 |
Copyright terms: Public domain | W3C validator |