![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exbidv | Unicode version |
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1416 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | albidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | exbidh 1502 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11ev 1706 2exbidv 1745 3exbidv 1746 eubidh 1903 eubid 1904 eleq1 2097 eleq2 2098 rexbidv2 2323 ceqsex2 2588 alexeq 2664 ceqex 2665 sbc5 2781 sbcex2 2806 sbcexg 2807 sbcabel 2833 eluni 3574 csbunig 3579 intab 3635 cbvopab1 3821 cbvopab1s 3823 axsep2 3867 zfauscl 3868 bnd2 3917 mss 3953 opeqex 3977 euotd 3982 snnex 4147 uniuni 4149 regexmid 4219 nnregexmid 4285 opeliunxp 4338 csbxpg 4364 brcog 4445 elrn2g 4468 dfdmf 4471 csbdmg 4472 eldmg 4473 dfrnf 4518 elrn2 4519 elrnmpt1 4528 brcodir 4655 xp11m 4702 xpimasn 4712 csbrng 4725 elxp4 4751 elxp5 4752 dfco2a 4764 cores 4767 funimaexglem 4925 brprcneu 5114 ssimaexg 5178 dmfco 5184 fndmdif 5215 fmptco 5273 fliftf 5382 acexmidlem2 5452 acexmidlemv 5453 cbvoprab1 5518 cbvoprab2 5519 dmtpos 5812 tfrlemi1 5887 ecdmn0m 6084 ereldm 6085 elqsn0m 6110 bren 6164 brdomg 6165 domeng 6169 recexnq 6374 prarloc 6486 genpdflem 6490 genpassl 6507 genpassu 6508 ltexprlemell 6572 ltexprlemelu 6573 ltexprlemm 6574 recexprlemell 6594 recexprlemelu 6595 bdsep2 9341 bdzfauscl 9345 strcoll2 9443 |
Copyright terms: Public domain | W3C validator |