![]() |
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 1528 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralbida 2471 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 |
This theorem is referenced by: raleqbidva 2686 poinxp 4692 funimass4 5562 fnmptfvd 5616 funimass3 5628 funconstss 5630 cocan1 5782 cocan2 5783 isocnv2 5807 isores2 5808 isoini2 5814 ofrfval 6085 ofrfval2 6093 dfsmo2 6282 smores 6287 smores2 6289 ac6sfi 6892 supisolem 7001 ordiso2 7028 ismkvnex 7147 nninfwlporlemd 7164 caucvgsrlemcau 7780 suplocsrlempr 7794 axsuploc 8017 suprleubex 8897 dfinfre 8899 zextlt 9331 prime 9338 infregelbex 9584 fzshftral 10091 fimaxq 10788 clim 11270 clim2 11272 clim2c 11273 clim0c 11275 climabs0 11296 climrecvg1n 11337 mertenslem2 11525 mertensabs 11526 dfgcd2 11995 sqrt2irr 12142 pc11 12310 pcz 12311 1arith 12345 infpn2 12437 grpidpropdg 12682 mndpropd 12730 grppropd 12780 ringpropd 13040 oppr1g 13074 tgss2 13243 neipsm 13318 ssidcn 13374 lmbrf 13379 cnnei 13396 cnrest2 13400 lmss 13410 lmres 13412 ismet2 13518 elmopn2 13613 metss 13658 metrest 13670 metcnp 13676 metcnp2 13677 metcn 13678 txmetcnp 13682 divcnap 13719 elcncf2 13725 mulc1cncf 13740 cncfmet 13743 cdivcncfap 13751 limcdifap 13795 limcmpted 13796 cnlimc 13805 2sqlem6 14120 iswomni0 14452 |
Copyright terms: Public domain | W3C validator |