Metamath Proof Explorer


Theorem opelopabb

Description: Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023)

Ref Expression
Hypotheses opelopabb.xph φ x φ
opelopabb.yph φ y φ
opelopabb.xch φ x χ
opelopabb.ych φ y χ
opelopabb.is φ x = A y = B ψ χ
Assertion opelopabb φ A B x y | ψ A V B V χ

Proof

Step Hyp Ref Expression
1 opelopabb.xph φ x φ
2 opelopabb.yph φ y φ
3 opelopabb.xch φ x χ
4 opelopabb.ych φ y χ
5 opelopabb.is φ x = A y = B ψ χ
6 elopab A B x y | ψ x y A B = x y ψ
7 1 2 3 4 5 copsex2b φ x y A B = x y ψ A V B V χ
8 6 7 syl5bb φ A B x y | ψ A V B V χ