theorem elFst (A: set) (a: nat): $ a e. Fst A <-> b0 a e. A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _1 = a -> _1 = a |
|
2 | 1 | b0eqd | _1 = a -> b0 _1 = b0 a |
3 | eqsidd | _1 = a -> A == A |
|
4 | 2, 3 | eleqd | _1 = a -> (b0 _1 e. A <-> b0 a e. A) |
5 | 4 | elabe | a e. {_1 | b0 _1 e. A} <-> b0 a e. A |
6 | 5 | conv Fst | a e. Fst A <-> b0 a e. A |