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	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	opabbidv	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		opabbidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2	1	anbi2d	$$⊢\phi \to \left(\left(z=⟨x,y⟩\wedge \psi \right)\leftrightarrow \left(z=⟨x,y⟩\wedge \chi \right)\right)$$
3	2	2exbidv	$$⊢\phi \to \left(\exists x\exists y\left(z=⟨x,y⟩\wedge \psi \right)\leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \chi \right)\right)$$
4	3	abbidv	$$⊢\phi \to \left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \psi \right)\right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \chi \right)\right\}$$
5		df-opab	$$⊢\left\{⟨x,y⟩|\psi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \psi \right)\right\}$$
6		df-opab	$$⊢\left\{⟨x,y⟩|\chi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \chi \right)\right\}$$
7	4 5 6	3eqtr4g	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\chi \right\}$$