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