cbvopab2

Description: Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013)

Step	Hyp	Ref	Expression
1		cbvopab2.1	$⊢ Ⅎ z φ$
2		cbvopab2.2	$⊢ Ⅎ y ψ$
3		cbvopab2.3	$⊢ y = z \to (φ \leftrightarrow ψ)$
4		nfv	$⊢ Ⅎ z w = ⟨x, y⟩$
5	4 1	nfan	$⊢ Ⅎ z (w = ⟨x, y⟩ \land φ)$
6		nfv	$⊢ Ⅎ y w = ⟨x, z⟩$
7	6 2	nfan	$⊢ Ⅎ y (w = ⟨x, z⟩ \land ψ)$
8		opeq2	$⊢ y = z \to ⟨x, y⟩ = ⟨x, z⟩$
9	8	eqeq2d	$⊢ y = z \to (w = ⟨x, y⟩ \leftrightarrow w = ⟨x, z⟩)$
10	9 3	anbi12d	$⊢ y = z \to ((w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨x, z⟩ \land ψ))$
11	5 7 10	cbvexv1	$⊢ \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists z (w = ⟨x, z⟩ \land ψ)$
12	11	exbii	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists z (w = ⟨x, z⟩ \land ψ)$
13	12	abbii	$⊢ \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists x \exists z (w = ⟨x, z⟩ \land ψ)\}$
14		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
15		df-opab	$⊢ \{⟨x, z⟩ \| ψ\} = \{w \| \exists x \exists z (w = ⟨x, z⟩ \land ψ)\}$
16	13 14 15	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨x, z⟩ \| ψ\}$

Metamath Proof Explorer