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 1521 | . 2 | |
2 | ralrimiv.1 | . 2 | |
3 | 1, 2 | ralrimi 2541 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2141 wral 2448 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 |
This theorem is referenced by: ralrimiva 2543 ralrimivw 2544 ralrimivv 2551 r19.27av 2605 rr19.3v 2869 rabssdv 3227 rzal 3512 trin 4097 class2seteq 4149 ralxfrALT 4452 ssorduni 4471 ordsucim 4484 onintonm 4501 issref 4993 funimaexglem 5281 resflem 5660 poxp 6211 rdgss 6362 dom2lem 6750 supisoti 6987 ordiso2 7012 updjud 7059 uzind 9323 zindd 9330 lbzbi 9575 icoshftf1o 9948 maxabslemval 11172 xrmaxiflemval 11213 fisum0diag2 11410 alzdvds 11814 hashgcdeq 12193 tgcl 12858 distop 12879 neiuni 12955 cnpnei 13013 isxmetd 13141 fsumcncntop 13350 bj-nntrans2 13987 bj-inf2vnlem1 14005 |
Copyright terms: Public domain | W3C validator |