let x be Element of Class F₂(); :: thesis: P₁[x]
ex y being object st
( y in F₁() & x = Class (F₂(),y) ) by EQREL_1:def 3;
hence P₁[x] by A1; :: thesis: verum