cbvopab1s

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003)

		Ref	Expression
	Assertion	cbvopab1s	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, y⟩ \| [z/ x] φ\}$

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ z \exists y (w = ⟨x, y⟩ \land φ)$
2		nfv	$⊢ Ⅎ x w = ⟨z, y⟩$
3		nfs1v	$⊢ Ⅎ x [z/ x] φ$
4	2 3	nfan	$⊢ Ⅎ x (w = ⟨z, y⟩ \land [z/ x] φ)$
5	4	nfex	$⊢ Ⅎ x \exists y (w = ⟨z, y⟩ \land [z/ x] φ)$
6		opeq1	$⊢ x = z \to ⟨x, y⟩ = ⟨z, y⟩$
7	6	eqeq2d	$⊢ x = z \to (w = ⟨x, y⟩ \leftrightarrow w = ⟨z, y⟩)$
8		sbequ12	$⊢ x = z \to (φ \leftrightarrow [z/ x] φ)$
9	7 8	anbi12d	$⊢ x = z \to ((w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨z, y⟩ \land [z/ x] φ))$
10	9	exbidv	$⊢ x = z \to (\exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (w = ⟨z, y⟩ \land [z/ x] φ))$
11	1 5 10	cbvexv1	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land [z/ x] φ)$
12	11	abbii	$⊢ \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land [z/ x] φ)\}$
13		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
14		df-opab	$⊢ \{⟨z, y⟩ \| [z/ x] φ\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land [z/ x] φ)\}$
15	12 13 14	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, y⟩ \| [z/ x] φ\}$

Metamath Proof Explorer