Metamath Proof Explorer


Theorem dmopabelb

Description: A set is an element of the domain of a ordered pair class abstraction iff there is a second set so that both sets fulfil the wff of the class abstraction. (Contributed by AV, 19-Oct-2023)

Ref Expression
Hypothesis dmopabel.d x = X φ ψ
Assertion dmopabelb X V X dom x y | φ y ψ

Proof

Step Hyp Ref Expression
1 dmopabel.d x = X φ ψ
2 dmopab dom x y | φ = x | y φ
3 2 eleq2i X dom x y | φ X x | y φ
4 1 exbidv x = X y φ y ψ
5 eqid x | y φ = x | y φ
6 4 5 elab2g X V X x | y φ y ψ
7 3 6 syl5bb X V X dom x y | φ y ψ