Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exbidv | GIF 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 1419 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1505 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∃wex 1381 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11ev 1709 2exbidv 1748 3exbidv 1749 eubidh 1906 eubid 1907 eleq1 2100 eleq2 2101 rexbidv2 2329 ceqsex2 2594 alexeq 2670 ceqex 2671 sbc5 2787 sbcex2 2812 sbcexg 2813 sbcabel 2839 eluni 3583 csbunig 3588 intab 3644 cbvopab1 3830 cbvopab1s 3832 axsep2 3876 zfauscl 3877 bnd2 3926 mss 3962 opeqex 3986 euotd 3991 snnex 4181 uniuni 4183 regexmid 4260 reg2exmid 4261 onintexmid 4297 reg3exmid 4304 nnregexmid 4342 opeliunxp 4395 csbxpg 4421 brcog 4502 elrn2g 4525 dfdmf 4528 csbdmg 4529 eldmg 4530 dfrnf 4575 elrn2 4576 elrnmpt1 4585 brcodir 4712 xp11m 4759 xpimasn 4769 csbrng 4782 elxp4 4808 elxp5 4809 dfco2a 4821 cores 4824 funimaexglem 4982 brprcneu 5171 ssimaexg 5235 dmfco 5241 fndmdif 5272 fmptco 5330 fliftf 5439 acexmidlem2 5509 acexmidlemv 5510 cbvoprab1 5576 cbvoprab2 5577 dmtpos 5871 tfrlemi1 5946 ecdmn0m 6148 ereldm 6149 elqsn0m 6174 bren 6228 brdomg 6229 domeng 6233 ac6sfi 6352 ordiso 6358 recexnq 6488 prarloc 6601 genpdflem 6605 genpassl 6622 genpassu 6623 ltexprlemell 6696 ltexprlemelu 6697 ltexprlemm 6698 recexprlemell 6720 recexprlemelu 6721 sumeq1 9874 bdsep2 10006 bdzfauscl 10010 strcoll2 10108 |
Copyright terms: Public domain | W3C validator |