![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralrimiva | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
Ref | Expression |
---|---|
ralrimiva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralrimiva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimiva.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralrimiv 2385 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 |
This theorem is referenced by: ralrimivvva 2396 rgen2 2399 rgen3 2400 nrexdv 2406 r19.29vva 2450 rabbidva 2542 ssrabdv 3013 ss2rabdv 3015 iuneq2dv 3669 disjeq2dv 3741 mpteq12dva 3829 triun 3858 issod 4047 peano2 4261 fun11iun 5090 fniinfv 5174 eqfnfv 5208 eqfnfvd 5211 dff3im 5255 dffo4 5258 foco2 5261 fmptd 5265 ffnfv 5266 fmpt2d 5270 ffvresb 5271 fconst2g 5319 fconstfvm 5322 resfunexg 5325 eufnfv 5332 fniunfv 5344 fcofo 5367 fliftel 5376 fliftfun 5379 fliftfuns 5381 riota5f 5435 grprinvlem 5637 grprinvd 5638 f1ocnvd 5644 suppssov1 5651 offval2 5668 ofrfval2 5669 offveqb 5672 caofref 5674 caofinvl 5675 opabex3d 5690 tfrlem1 5864 tfrlemisucaccv 5880 tfrlemiubacc 5885 omcl 5980 oeicl 5981 qliftfuns 6126 genprndl 6504 genprndu 6505 nqprloc 6528 ltexprlemrnd 6579 ltexprlemdisj 6580 recexprlemrnd 6601 recexprlemdisj 6602 caucvgprlemlim 6652 negeu 6999 creur 7692 creui 7693 indstr2 8322 iooidg 8548 iccsupr 8605 icoshftf1o 8629 fznlem 8675 frecuzrdgfn 8879 iseqovex 8899 iseqval 8900 iseqfn 8901 iseq1 8902 iseqcl 8903 iseqp1 8904 iseqfveq2 8905 iseqfveq 8907 |
Copyright terms: Public domain | W3C validator |