Metamath Proof Explorer


Theorem elrnmpoid

Description: Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis elrnmpoid.1 F=xA,yBC
Assertion elrnmpoid xAyBxAyBCVxFyranF

Proof

Step Hyp Ref Expression
1 elrnmpoid.1 F=xA,yBC
2 1 fnmpo xAyBCVFFnA×B
3 2 3ad2ant3 xAyBxAyBCVFFnA×B
4 simp1 xAyBxAyBCVxA
5 simp2 xAyBxAyBCVyB
6 fnovrn FFnA×BxAyBxFyranF
7 3 4 5 6 syl3anc xAyBxAyBCVxFyranF