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		nfv	$$⊢Ⅎx\phi$$
3		nfv	$$⊢Ⅎy\phi$$
4		nfv	$$⊢Ⅎz\phi$$
5	2 3 4 1	oprabbid	$$⊢\phi \to \left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{⟨⟨x,y⟩,z⟩|\chi \right\}$$