![]() |
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 1509 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rexbida 2433 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-rex 2423 |
This theorem is referenced by: 2rexbiia 2454 2rexbidva 2461 rexeqbidva 2644 dfimafn 5478 funimass4 5480 fconstfvm 5646 fliftel 5702 fliftf 5708 f1oiso 5735 releldm2 6091 frecabcl 6304 qsinxp 6513 qliftel 6517 supisolem 6903 enumctlemm 7007 ismkvnex 7037 genpassl 7356 genpassu 7357 addcomprg 7410 mulcomprg 7412 1idprl 7422 1idpru 7423 archrecnq 7495 archrecpr 7496 caucvgprprlemexbt 7538 caucvgprprlemexb 7539 archsr 7614 map2psrprg 7637 suplocsrlempr 7639 axsuploc 7861 cnegexlem3 7963 cnegex2 7965 recexre 8364 rerecclap 8514 creur 8741 creui 8742 nndiv 8785 arch 8998 nnrecl 8999 expnlbnd 10447 fimaxq 10605 clim2 11084 clim2c 11085 clim0c 11087 climabs0 11108 climrecvg1n 11149 sumeq2 11160 mertensabs 11338 prodeq2 11358 zproddc 11380 nndivides 11536 alzdvds 11588 oddm1even 11608 oddnn02np1 11613 oddge22np1 11614 evennn02n 11615 evennn2n 11616 divalgb 11658 modremain 11662 iscnp3 12411 lmbrf 12423 cncnp 12438 lmss 12454 metrest 12714 metcnp 12720 metcnp2 12721 txmetcnp 12726 cdivcncfap 12795 ivthdec 12830 pw1nct 13371 |
Copyright terms: Public domain | W3C validator |