Theorem opabbidv

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995)

	Ref	Expression
Hypothesis	opabbidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		opabbidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2	1	anbi2d	⊢ ( 𝜑 → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜒 ) ) )
3	2	2exbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜒 ) ) )
4	3	abbidv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜒 ) } )
5		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
6		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜒 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜒 ) }
7	4 5 6	3eqtr4g	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜒 } )