![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exbidv | Unicode version |
Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1507 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | albidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | exbidh 1594 |
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 |
This theorem is referenced by: ax11ev 1801 2exbidv 1841 3exbidv 1842 eubidh 2006 eubid 2007 eleq1w 2201 eleq2w 2202 eleq1 2203 eleq2 2204 rexbidv2 2441 ceqsex2 2729 alexeq 2815 ceqex 2816 sbc5 2936 sbcex2 2966 sbcexg 2967 sbcabel 2994 eluni 3747 csbunig 3752 intab 3808 cbvopab1 4009 cbvopab1s 4011 axsep2 4055 zfauscl 4056 bnd2 4105 mss 4156 opeqex 4179 euotd 4184 snnex 4377 uniuni 4380 regexmid 4458 reg2exmid 4459 onintexmid 4495 reg3exmid 4502 nnregexmid 4542 opeliunxp 4602 csbxpg 4628 brcog 4714 elrn2g 4737 dfdmf 4740 csbdmg 4741 eldmg 4742 dfrnf 4788 elrn2 4789 elrnmpt1 4798 brcodir 4934 xp11m 4985 xpimasn 4995 csbrng 5008 elxp4 5034 elxp5 5035 dfco2a 5047 cores 5050 funimaexglem 5214 brprcneu 5422 ssimaexg 5491 dmfco 5497 fndmdif 5533 fmptco 5594 fliftf 5708 acexmidlem2 5779 acexmidlemv 5780 cbvoprab1 5851 cbvoprab2 5852 oprssdmm 6077 dmtpos 6161 tfrlemi1 6237 tfr1onlemaccex 6253 tfrcllemaccex 6266 ecdmn0m 6479 ereldm 6480 elqsn0m 6505 mapsn 6592 bren 6649 brdomg 6650 domeng 6654 ac6sfi 6800 ordiso 6929 ctssdclemr 7005 enumct 7008 ctssexmid 7032 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 acfun 7080 ccfunen 7096 cc1 7097 cc2lem 7098 cc2 7099 cc3 7100 recexnq 7222 prarloc 7335 genpdflem 7339 genpassl 7356 genpassu 7357 ltexprlemell 7430 ltexprlemelu 7431 ltexprlemm 7432 recexprlemell 7454 recexprlemelu 7455 cnm 7664 sup3exmid 8739 seq3f1olemp 10306 zfz1isolem1 10615 zfz1iso 10616 sumeq1 11156 sumeq2 11160 summodc 11184 fsum3 11188 fsum2dlemstep 11235 ntrivcvgap0 11350 prodeq1f 11353 prodeq2w 11357 prodeq2 11358 prodmodc 11379 zproddc 11380 fprodseq 11384 ctinf 11979 ctiunct 11989 bdsep2 13255 bdzfauscl 13259 strcoll2 13352 sscoll2 13357 subctctexmid 13369 nninfall 13379 |
Copyright terms: Public domain | W3C validator |