| ∀ x0 x1 . x1 ⊆ x0 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|and (bij x0 x0 (ap x3)) (∀ x4 . x4 ∈ x1 ⟶ ap x3 x4 = x4)} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setexp x0 x0|and (bij x0 x0 (ap x4)) (∀ x5 . x5 ∈ x1 ⟶ ap x4 x5 = x5)} ⟶ lam x0 (λ x4 . ap x3 (ap x2 x4)) ∈ {x4 ∈ setexp x0 x0|and (bij x0 x0 (ap x4)) (∀ x5 . x5 ∈ x1 ⟶ ap x4 x5 = x5)} |
|