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