This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oprabbid

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

		Ref	Expression
	Hypotheses	oprabbid.1	$⊢ Ⅎ x φ$
		oprabbid.2	$⊢ Ⅎ y φ$
		oprabbid.3	$⊢ Ⅎ z φ$
		oprabbid.4	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	oprabbid	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨⟨x, y⟩, z⟩ \| χ\}$

Proof

Step	Hyp	Ref	Expression
1		oprabbid.1	$⊢ Ⅎ x φ$
2		oprabbid.2	$⊢ Ⅎ y φ$
3		oprabbid.3	$⊢ Ⅎ z φ$
4		oprabbid.4	$⊢ φ \to (ψ \leftrightarrow χ)$
5	4	anbi2d	$⊢ φ \to ((w = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow (w = ⟨⟨x, y⟩, z⟩ \land χ))$
6	3 5	exbid	$⊢ φ \to (\exists z (w = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow \exists z (w = ⟨⟨x, y⟩, z⟩ \land χ))$
7	2 6	exbid	$⊢ φ \to (\exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land χ))$
8	1 7	exbid	$⊢ φ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land χ))$
9	8	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 χ)\}$
10		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ψ)\}$
11		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| χ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land χ)\}$
12	9 10 11	3eqtr4g	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨⟨x, y⟩, z⟩ \| χ\}$