Add phplem4 to iset.mm
Add phplem4 to iset.mm

Copied from set.mm with only one small change: in the proof, we need to
supply hypotheses to fvex (but this is easy).

metamath/set.mm,metamath/set.mm,metamath/set.mm