Metamath Proof Explorer


Theorem dif1o

Description: Two ways to say that A is a nonzero number of the set B . (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion dif1o AB1𝑜ABA

Proof

Step Hyp Ref Expression
1 df1o2 1𝑜=
2 1 difeq2i B1𝑜=B
3 2 eleq2i AB1𝑜AB
4 eldifsn ABABA
5 3 4 bitri AB1𝑜ABA