Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexbidva | Unicode version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 |
Ref | Expression |
---|---|
rexbidva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1524 | . 2 | |
2 | ralbidva.1 | . 2 | |
3 | 1, 2 | rexbida 2468 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 104 wb 105 wcel 2144 wrex 2452 |
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 1443 ax-gen 1445 ax-ie1 1489 ax-ie2 1490 ax-4 1506 ax-17 1522 ax-ial 1530 |
This theorem depends on definitions: df-bi 117 df-nf 1457 df-rex 2457 |
This theorem is referenced by: 2rexbiia 2489 2rexbidva 2496 rexeqbidva 2683 dfimafn 5553 funimass4 5555 fconstfvm 5723 fliftel 5781 fliftf 5787 f1oiso 5814 releldm2 6173 frecabcl 6387 qsinxp 6598 qliftel 6602 supisolem 6994 enumctlemm 7100 ismkvnex 7140 genpassl 7495 genpassu 7496 addcomprg 7549 mulcomprg 7551 1idprl 7561 1idpru 7562 archrecnq 7634 archrecpr 7635 caucvgprprlemexbt 7677 caucvgprprlemexb 7678 archsr 7753 map2psrprg 7776 suplocsrlempr 7778 axsuploc 8001 cnegexlem3 8105 cnegex2 8107 recexre 8506 rerecclap 8656 creur 8884 creui 8885 nndiv 8928 arch 9141 nnrecl 9142 expnlbnd 10609 fimaxq 10771 clim2 11255 clim2c 11256 clim0c 11258 climabs0 11279 climrecvg1n 11320 sumeq2 11331 mertensabs 11509 prodeq2 11529 zproddc 11551 nndivides 11768 alzdvds 11823 oddm1even 11843 oddnn02np1 11848 oddge22np1 11849 evennn02n 11850 evennn2n 11851 divalgb 11893 modremain 11897 modprmn0modprm0 12219 pythagtriplem2 12229 pythagtrip 12246 pceu 12258 mndpfo 12701 mndpropd 12703 grppropd 12751 iscnp3 13160 lmbrf 13172 cncnp 13187 lmss 13203 metrest 13463 metcnp 13469 metcnp2 13470 txmetcnp 13475 cdivcncfap 13544 ivthdec 13579 pw1nct 14199 |
Copyright terms: Public domain | W3C validator |