Theorem opabbid

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Hypotheses	opabbid.1	$$⊢Ⅎx\phi$$
	opabbid.2	$$⊢Ⅎy\phi$$
	opabbid.3	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	opabbid	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		opabbid.1	$$⊢Ⅎx\phi$$
2		opabbid.2	$$⊢Ⅎy\phi$$
3		opabbid.3	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
4	3	anbi2d	$$⊢\phi \to \left(\left(z=⟨x,y⟩\wedge \psi \right)\leftrightarrow \left(z=⟨x,y⟩\wedge \chi \right)\right)$$
5	2 4	exbid	$$⊢\phi \to \left(\exists y\left(z=⟨x,y⟩\wedge \psi \right)\leftrightarrow \exists y\left(z=⟨x,y⟩\wedge \chi \right)\right)$$
6	1 5	exbid	$$⊢\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)$$
7	6	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\}$$
8		df-opab	$$⊢\left\{⟨x,y⟩|\psi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \psi \right)\right\}$$
9		df-opab	$$⊢\left\{⟨x,y⟩|\chi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \chi \right)\right\}$$
10	7 8 9	3eqtr4g	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}=\left\{⟨x,y⟩|\chi \right\}$$