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 ( 𝑥 = 𝑋 → ( 𝜑𝜓 ) )
Assertion dmopabelb ( 𝑋𝑉 → ( 𝑋 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑦 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dmopabel.d ( 𝑥 = 𝑋 → ( 𝜑𝜓 ) )
2 dmopab dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 }
3 2 eleq2i ( 𝑋 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝜑 } )
4 1 exbidv ( 𝑥 = 𝑋 → ( ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜓 ) )
5 eqid { 𝑥 ∣ ∃ 𝑦 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 }
6 4 5 elab2g ( 𝑋𝑉 → ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝜑 } ↔ ∃ 𝑦 𝜓 ) )
7 3 6 syl5bb ( 𝑋𝑉 → ( 𝑋 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑦 𝜓 ) )