theorem appT (A B: set) (f x: nat): $ f e. Arrow A B /\ x e. A -> f @ x e. B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elArrow | f e. Arrow A B <-> func f A B |
|
| 2 | 1 | aneq1i | f e. Arrow A B /\ x e. A <-> func f A B /\ x e. A |
| 3 | funcT | func f A B /\ x e. A -> f @ x e. B |
|
| 4 | 2, 3 | sylbi | f e. Arrow A B /\ x e. A -> f @ x e. B |