cbvopab1

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbvopab1g for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1.1	$⊢ Ⅎ z φ$
2		cbvopab1.2	$⊢ Ⅎ x ψ$
3		cbvopab1.3	$⊢ x = z \to (φ \leftrightarrow ψ)$
4		nfv	$⊢ Ⅎ v \exists y (w = ⟨x, y⟩ \land φ)$
5		nfv	$⊢ Ⅎ x w = ⟨v, y⟩$
6		nfs1v	$⊢ Ⅎ x [v/ x] φ$
7	5 6	nfan	$⊢ Ⅎ x (w = ⟨v, y⟩ \land [v/ x] φ)$
8	7	nfex	$⊢ Ⅎ x \exists y (w = ⟨v, y⟩ \land [v/ x] φ)$
9		opeq1	$⊢ x = v \to ⟨x, y⟩ = ⟨v, y⟩$
10	9	eqeq2d	$⊢ x = v \to (w = ⟨x, y⟩ \leftrightarrow w = ⟨v, y⟩)$
11		sbequ12	$⊢ x = v \to (φ \leftrightarrow [v/ x] φ)$
12	10 11	anbi12d	$⊢ x = v \to ((w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨v, y⟩ \land [v/ x] φ))$
13	12	exbidv	$⊢ x = v \to (\exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (w = ⟨v, y⟩ \land [v/ x] φ))$
14	4 8 13	cbvexv1	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists v \exists y (w = ⟨v, y⟩ \land [v/ x] φ)$
15		nfv	$⊢ Ⅎ z w = ⟨v, y⟩$
16	1	nfsbv	$⊢ Ⅎ z [v/ x] φ$
17	15 16	nfan	$⊢ Ⅎ z (w = ⟨v, y⟩ \land [v/ x] φ)$
18	17	nfex	$⊢ Ⅎ z \exists y (w = ⟨v, y⟩ \land [v/ x] φ)$
19		nfv	$⊢ Ⅎ v \exists y (w = ⟨z, y⟩ \land ψ)$
20		opeq1	$⊢ v = z \to ⟨v, y⟩ = ⟨z, y⟩$
21	20	eqeq2d	$⊢ v = z \to (w = ⟨v, y⟩ \leftrightarrow w = ⟨z, y⟩)$
22	2 3	sbhypf	$⊢ v = z \to ([v/ x] φ \leftrightarrow ψ)$
23	21 22	anbi12d	$⊢ v = z \to ((w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow (w = ⟨z, y⟩ \land ψ))$
24	23	exbidv	$⊢ v = z \to (\exists y (w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow \exists y (w = ⟨z, y⟩ \land ψ))$
25	18 19 24	cbvexv1	$⊢ \exists v \exists y (w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land ψ)$
26	14 25	bitri	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land ψ)$
27	26	abbii	$⊢ \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
28		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
29		df-opab	$⊢ \{⟨z, y⟩ \| ψ\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
30	27 28 29	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, y⟩ \| ψ\}$

Metamath Proof Explorer

Theorem cbvopab1

Proof