oprabbidv

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

		Ref	Expression
	Hypothesis	oprabbidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	oprabbidv	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨⟨x, y⟩, z⟩ \| χ\}$

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

Metamath Proof Explorer