Theorem 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	⊢ Ⅎ 𝑧 𝜑
	cbvopab.2	⊢ Ⅎ 𝑤 𝜑
	cbvopab.3	⊢ Ⅎ 𝑥 𝜓
	cbvopab.4	⊢ Ⅎ 𝑦 𝜓
	cbvopab.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvopab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvopab.1	⊢ Ⅎ 𝑧 𝜑
2		cbvopab.2	⊢ Ⅎ 𝑤 𝜑
3		cbvopab.3	⊢ Ⅎ 𝑥 𝜓
4		cbvopab.4	⊢ Ⅎ 𝑦 𝜓
5		cbvopab.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
6		nfv	⊢ Ⅎ 𝑧 𝑣 = ⟨ 𝑥 , 𝑦 ⟩
7	6 1	nfan	⊢ Ⅎ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
8		nfv	⊢ Ⅎ 𝑤 𝑣 = ⟨ 𝑥 , 𝑦 ⟩
9	8 2	nfan	⊢ Ⅎ 𝑤 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
10		nfv	⊢ Ⅎ 𝑥 𝑣 = ⟨ 𝑧 , 𝑤 ⟩
11	10 3	nfan	⊢ Ⅎ 𝑥 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 )
12		nfv	⊢ Ⅎ 𝑦 𝑣 = ⟨ 𝑧 , 𝑤 ⟩
13	12 4	nfan	⊢ Ⅎ 𝑦 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 )
14		opeq12	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
15	14	eqeq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ) )
16	15 5	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) ) )
17	7 9 11 13 16	cbvex2v	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) )
18	17	abbii	⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) }
19		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
20		df-opab	⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 } = { 𝑣 ∣ ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝜓 ) }
21	18 19 20	3eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }