Metamath Proof Explorer


Theorem ind1a

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

Ref Expression
Assertion ind1a O V A O X O 𝟙 O A X = 1 X A

Proof

Step Hyp Ref Expression
1 indfval O V A O X O 𝟙 O A X = if X A 1 0
2 1 eqeq1d O V A O X O 𝟙 O A X = 1 if X A 1 0 = 1
3 eqid 1 = 1
4 3 biantru X A X A 1 = 1
5 ax-1ne0 1 0
6 5 neii ¬ 1 = 0
7 6 biorfi X A 1 = 1 X A 1 = 1 1 = 0
8 6 bianfi 1 = 0 ¬ X A 1 = 0
9 8 orbi2i X A 1 = 1 1 = 0 X A 1 = 1 ¬ X A 1 = 0
10 4 7 9 3bitri X A X A 1 = 1 ¬ X A 1 = 0
11 eqif 1 = if X A 1 0 X A 1 = 1 ¬ X A 1 = 0
12 eqcom 1 = if X A 1 0 if X A 1 0 = 1
13 10 11 12 3bitr2ri if X A 1 0 = 1 X A
14 2 13 bitrdi O V A O X O 𝟙 O A X = 1 X A