Theorem oprabbidv

Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004)

	Ref	Expression
Hypothesis	oprabbidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	oprabbidv	$$⊢\phi \to \left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{⟨⟨x,y⟩,z⟩|\chi \right\}$$

Proof

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