cbvopab1g

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbvopab1 for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1g.1	$⊢ Ⅎ z φ$
2		cbvopab1g.2	$⊢ Ⅎ x ψ$
3		cbvopab1g.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	nfsb	$⊢ Ⅎ 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		sbequ	$⊢ v = z \to ([v/ x] φ \leftrightarrow [z/ x] φ)$
23	2 3	sbie	$⊢ [z/ x] φ \leftrightarrow ψ$
24	22 23	bitrdi	$⊢ v = z \to ([v/ x] φ \leftrightarrow ψ)$
25	21 24	anbi12d	$⊢ v = z \to ((w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow (w = ⟨z, y⟩ \land ψ))$
26	25	exbidv	$⊢ v = z \to (\exists y (w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow \exists y (w = ⟨z, y⟩ \land ψ))$
27	18 19 26	cbvexv1	$⊢ \exists v \exists y (w = ⟨v, y⟩ \land [v/ x] φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land ψ)$
28	14 27	bitri	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists z \exists y (w = ⟨z, y⟩ \land ψ)$
29	28	abbii	$⊢ \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
30		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
31		df-opab	$⊢ \{⟨z, y⟩ \| ψ\} = \{w \| \exists z \exists y (w = ⟨z, y⟩ \land ψ)\}$
32	29 30 31	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, y⟩ \| ψ\}$

Metamath Proof Explorer

Theorem cbvopab1g

Proof