Metamath Proof Explorer


Theorem opabssxpd

Description: An ordered-pair class abstraction is a subset of a Cartesian product. Formerly part of proof for opabex2 . (Contributed by AV, 26-Nov-2021)

Ref Expression
Hypotheses opabssxpd.x φ ψ x A
opabssxpd.y φ ψ y B
Assertion opabssxpd φ x y | ψ A × B

Proof

Step Hyp Ref Expression
1 opabssxpd.x φ ψ x A
2 opabssxpd.y φ ψ y B
3 df-opab x y | ψ = z | x y z = x y ψ
4 simprl φ z = x y ψ z = x y
5 1 2 opelxpd φ ψ x y A × B
6 5 adantrl φ z = x y ψ x y A × B
7 4 6 eqeltrd φ z = x y ψ z A × B
8 7 ex φ z = x y ψ z A × B
9 8 exlimdvv φ x y z = x y ψ z A × B
10 9 abssdv φ z | x y z = x y ψ A × B
11 3 10 eqsstrid φ x y | ψ A × B