Metamath Proof Explorer


Theorem elopabran

Description: Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021)

Ref Expression
Assertion elopabran A x y | x R y ψ A R

Proof

Step Hyp Ref Expression
1 simpl x R y ψ x R y
2 1 ssopab2i x y | x R y ψ x y | x R y
3 opabss x y | x R y R
4 2 3 sstri x y | x R y ψ R
5 4 sseli A x y | x R y ψ A R