Metamath Proof Explorer


Theorem elimag

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 20-Jan-2007)

Ref Expression
Assertion elimag AVABCxCxBA

Proof

Step Hyp Ref Expression
1 breq2 y=AxByxBA
2 1 rexbidv y=AxCxByxCxBA
3 dfima2 BC=y|xCxBy
4 2 3 elab2g AVABCxCxBA