Theorem 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	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑦 ⟩ ∣ [ 𝑧 / 𝑥 ] 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
2		nfv	⊢ Ⅎ 𝑥 𝑤 = ⟨ 𝑧 , 𝑦 ⟩
3		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
4	2 3	nfan	⊢ Ⅎ 𝑥 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 )
5	4	nfex	⊢ Ⅎ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 )
6		opeq1	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑦 ⟩ )
7	6	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ) )
8		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
9	7 8	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
10	9	exbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
11	1 5 10	cbvexv1	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
12	11	abbii	⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑤 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
13		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
14		df-opab	⊢ { ⟨ 𝑧 , 𝑦 ⟩ ∣ [ 𝑧 / 𝑥 ] 𝜑 } = { 𝑤 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ [ 𝑧 / 𝑥 ] 𝜑 ) }
15	12 13 14	3eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑦 ⟩ ∣ [ 𝑧 / 𝑥 ] 𝜑 }