Theorem abid2 ≪ | index | src | ≫

theorem abid2 (A: set) {x: nat}: $ {x | x e. A} == A $;

x = y -> (x e. A <-> y e. A)

y e. {x | x e. A} <-> y e. A

{x | x e. A} == A

Axiom use