![]() |
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 1526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | albidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | exbidh 1614 |
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 |
This theorem is referenced by: ax11ev 1828 2exbidv 1868 3exbidv 1869 eubidh 2032 eubid 2033 eleq1w 2238 eleq2w 2239 eleq1 2240 eleq2 2241 rexbidv2 2480 ceqsex2 2777 alexeq 2863 ceqex 2864 sbc5 2986 sbcex2 3016 sbcexg 3017 sbcabel 3044 eluni 3810 csbunig 3815 intab 3871 cbvopab1 4073 cbvopab1s 4075 axsep2 4119 zfauscl 4120 bnd2 4170 mss 4223 opeqex 4246 euotd 4251 snnex 4445 uniuni 4448 regexmid 4531 reg2exmid 4532 onintexmid 4569 reg3exmid 4576 nnregexmid 4617 opeliunxp 4678 csbxpg 4704 brcog 4790 elrn2g 4813 dfdmf 4816 csbdmg 4817 eldmg 4818 dfrnf 4864 elrn2 4865 elrnmpt1 4874 brcodir 5012 xp11m 5063 xpimasn 5073 csbrng 5086 elxp4 5112 elxp5 5113 dfco2a 5125 cores 5128 funimaexglem 5295 brprcneu 5504 ssimaexg 5574 dmfco 5580 fndmdif 5617 fmptco 5678 fliftf 5794 acexmidlem2 5866 acexmidlemv 5867 cbvoprab1 5941 cbvoprab2 5942 oprssdmm 6166 dmtpos 6251 tfrlemi1 6327 tfr1onlemaccex 6343 tfrcllemaccex 6356 ecdmn0m 6571 ereldm 6572 elqsn0m 6597 mapsn 6684 bren 6741 brdomg 6742 domeng 6746 ac6sfi 6892 ordiso 7029 ctssdclemr 7105 enumct 7108 ctssexmid 7142 exmidfodomrlemr 7195 exmidfodomrlemrALT 7196 acfun 7200 ccfunen 7251 cc1 7252 cc2lem 7253 cc2 7254 cc3 7255 recexnq 7377 prarloc 7490 genpdflem 7494 genpassl 7511 genpassu 7512 ltexprlemell 7585 ltexprlemelu 7586 ltexprlemm 7587 recexprlemell 7609 recexprlemelu 7610 cnm 7819 sup3exmid 8900 seq3f1olemp 10485 zfz1isolem1 10801 zfz1iso 10802 sumeq1 11344 sumeq2 11348 summodc 11372 fsum3 11376 fsum2dlemstep 11423 ntrivcvgap0 11538 prodeq1f 11541 prodeq2w 11545 prodeq2 11546 prodmodc 11567 zproddc 11568 fprodseq 11572 fprodntrivap 11573 fprod2dlemstep 11611 ctinf 12411 ctiunct 12421 ssomct 12426 bdsep2 14287 bdzfauscl 14291 strcoll2 14384 sscoll2 14389 subctctexmid 14399 nninfall 14407 |
Copyright terms: Public domain | W3C validator |