cbvopab1v

Description: Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003) (Proof shortened by Eric Schmidt, 4-Apr-2007) Reduce axiom usage. (Revised by GG, 17-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1v.1	$⊢ x = z \to (φ \leftrightarrow ψ)$
2		opeq1	$⊢ x = z \to ⟨x, y⟩ = ⟨z, y⟩$
3	2	eqeq2d	$⊢ x = z \to (w = ⟨x, y⟩ \leftrightarrow w = ⟨z, y⟩)$
4	3 1	anbi12d	$⊢ x = z \to ((w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨z, y⟩ \land ψ))$
5	4	exbidv	$⊢ x = z \to (\exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (w = ⟨z, y⟩ \land ψ))$
6	5	cbvexvw	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land ψ)$
7	6	abbii	$⊢ \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
8		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
9		df-opab	$⊢ \{⟨z, y⟩ \| ψ\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
10	7 8 9	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, y⟩ \| ψ\}$

Metamath Proof Explorer

Theorem cbvopab1v

Proof