Metamath Proof Explorer


Theorem opelresi

Description: Ordered pair membership in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995)

Ref Expression
Hypothesis opelresi.1 CV
Assertion opelresi BCRABABCR

Proof

Step Hyp Ref Expression
1 opelresi.1 CV
2 opelres CVBCRABABCR
3 1 2 ax-mp BCRABABCR