Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbidva | Unicode version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 |
Ref | Expression |
---|---|
ralbidva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1493 | . 2 | |
2 | ralbidva.1 | . 2 | |
3 | 1, 2 | ralbida 2408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 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: raleqbidva 2617 poinxp 4578 funimass4 5440 funimass3 5504 funconstss 5506 cocan1 5656 cocan2 5657 isocnv2 5681 isores2 5682 isoini2 5688 ofrfval 5958 ofrfval2 5966 dfsmo2 6152 smores 6157 smores2 6159 ac6sfi 6760 supisolem 6863 ordiso2 6888 ismkvnex 6997 caucvgsrlemcau 7569 suplocsrlempr 7583 axsuploc 7805 suprleubex 8680 dfinfre 8682 zextlt 9111 prime 9118 fzshftral 9856 fimaxq 10541 clim 11018 clim2 11020 clim2c 11021 clim0c 11023 climabs0 11044 climrecvg1n 11085 mertenslem2 11273 mertensabs 11274 dfgcd2 11629 sqrt2irr 11767 tgss2 12175 neipsm 12250 ssidcn 12306 lmbrf 12311 cnnei 12328 cnrest2 12332 lmss 12342 lmres 12344 ismet2 12450 elmopn2 12545 metss 12590 metrest 12602 metcnp 12608 metcnp2 12609 metcn 12610 txmetcnp 12614 divcnap 12651 elcncf2 12657 mulc1cncf 12672 cncfmet 12675 cdivcncfap 12683 limcdifap 12727 limcmpted 12728 cnlimc 12737 |
Copyright terms: Public domain | W3C validator |