cbvopab

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003)

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

Proof

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

Metamath Proof Explorer

Theorem cbvopab

Proof