Theorem restr_is_subclass

Proof
01. ⊢ f ∩ (A × UnivCl) ⊆ f, intersection_incl_left.
restr_is_subclass. ⊢ restr f A ⊆ f,
  eq_subst_rev restr_eq 1, P u ↔ u ⊆ f.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.