Metamath Proof Explorer


Theorem ind0

Description: Value of the indicator function where it is 0 . (Contributed by Thierry Arnoux, 14-Aug-2017)

Ref Expression
Assertion ind0 OVAOXOA𝟙OAX=0

Proof

Step Hyp Ref Expression
1 eldifi XOAXO
2 indfval OVAOXO𝟙OAX=ifXA10
3 1 2 syl3an3 OVAOXOA𝟙OAX=ifXA10
4 eldifn XOA¬XA
5 4 3ad2ant3 OVAOXOA¬XA
6 5 iffalsed OVAOXOAifXA10=0
7 3 6 eqtrd OVAOXOA𝟙OAX=0