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 1491 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | exbidh 1578 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wex 1453 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11ev 1784 2exbidv 1824 3exbidv 1825 eubidh 1983 eubid 1984 eleq1w 2178 eleq2w 2179 eleq1 2180 eleq2 2181 rexbidv2 2417 ceqsex2 2700 alexeq 2785 ceqex 2786 sbc5 2905 sbcex2 2934 sbcexg 2935 sbcabel 2962 eluni 3709 csbunig 3714 intab 3770 cbvopab1 3971 cbvopab1s 3973 axsep2 4017 zfauscl 4018 bnd2 4067 mss 4118 opeqex 4141 euotd 4146 snnex 4339 uniuni 4342 regexmid 4420 reg2exmid 4421 onintexmid 4457 reg3exmid 4464 nnregexmid 4504 opeliunxp 4564 csbxpg 4590 brcog 4676 elrn2g 4699 dfdmf 4702 csbdmg 4703 eldmg 4704 dfrnf 4750 elrn2 4751 elrnmpt1 4760 brcodir 4896 xp11m 4947 xpimasn 4957 csbrng 4970 elxp4 4996 elxp5 4997 dfco2a 5009 cores 5012 funimaexglem 5176 brprcneu 5382 ssimaexg 5451 dmfco 5457 fndmdif 5493 fmptco 5554 fliftf 5668 acexmidlem2 5739 acexmidlemv 5740 cbvoprab1 5811 cbvoprab2 5812 oprssdmm 6037 dmtpos 6121 tfrlemi1 6197 tfr1onlemaccex 6213 tfrcllemaccex 6226 ecdmn0m 6439 ereldm 6440 elqsn0m 6465 mapsn 6552 bren 6609 brdomg 6610 domeng 6614 ac6sfi 6760 ordiso 6889 ctssdclemr 6965 enumct 6968 ctssexmid 6992 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 acfun 7031 ccfunen 7047 recexnq 7166 prarloc 7279 genpdflem 7283 genpassl 7300 genpassu 7301 ltexprlemell 7374 ltexprlemelu 7375 ltexprlemm 7376 recexprlemell 7398 recexprlemelu 7399 cnm 7608 sup3exmid 8683 seq3f1olemp 10243 zfz1isolem1 10551 zfz1iso 10552 sumeq1 11092 sumeq2 11096 summodc 11120 fsum3 11124 fsum2dlemstep 11171 ctinf 11870 ctiunct 11880 bdsep2 13011 bdzfauscl 13015 strcoll2 13108 subctctexmid 13123 nninfall 13131 |
Copyright terms: Public domain | W3C validator |