![]() |
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 1528 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rexbida 2472 |
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-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-rex 2461 |
This theorem is referenced by: 2rexbiia 2493 2rexbidva 2500 rexeqbidva 2687 dfimafn 5563 funimass4 5565 fconstfvm 5733 fliftel 5791 fliftf 5797 f1oiso 5824 releldm2 6183 frecabcl 6397 qsinxp 6608 qliftel 6612 supisolem 7004 enumctlemm 7110 ismkvnex 7150 genpassl 7520 genpassu 7521 addcomprg 7574 mulcomprg 7576 1idprl 7586 1idpru 7587 archrecnq 7659 archrecpr 7660 caucvgprprlemexbt 7702 caucvgprprlemexb 7703 archsr 7778 map2psrprg 7801 suplocsrlempr 7803 axsuploc 8026 cnegexlem3 8130 cnegex2 8132 recexre 8531 rerecclap 8683 creur 8912 creui 8913 nndiv 8956 arch 9169 nnrecl 9170 expnlbnd 10639 fimaxq 10800 clim2 11284 clim2c 11285 clim0c 11287 climabs0 11308 climrecvg1n 11349 sumeq2 11360 mertensabs 11538 prodeq2 11558 zproddc 11580 nndivides 11797 alzdvds 11852 oddm1even 11872 oddnn02np1 11877 oddge22np1 11878 evennn02n 11879 evennn2n 11880 divalgb 11922 modremain 11926 modprmn0modprm0 12248 pythagtriplem2 12258 pythagtrip 12275 pceu 12287 mndpfo 12771 mndpropd 12773 grppropd 12825 dvdsr02 13205 crngunit 13211 dvdsrpropdg 13247 iscnp3 13574 lmbrf 13586 cncnp 13601 lmss 13617 metrest 13877 metcnp 13883 metcnp2 13884 txmetcnp 13889 cdivcncfap 13958 ivthdec 13993 pw1nct 14612 |
Copyright terms: Public domain | W3C validator |