Theorem cbvoprab3

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013)

	Ref	Expression
Hypotheses	cbvoprab3.1	⊢ Ⅎ 𝑤 𝜑
	cbvoprab3.2	⊢ Ⅎ 𝑧 𝜓
	cbvoprab3.3	⊢ ( 𝑧 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvoprab3	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvoprab3.1	⊢ Ⅎ 𝑤 𝜑
2		cbvoprab3.2	⊢ Ⅎ 𝑧 𝜓
3		cbvoprab3.3	⊢ ( 𝑧 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑤 𝑣 = ⟨ 𝑥 , 𝑦 ⟩
5	4 1	nfan	⊢ Ⅎ 𝑤 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
6	5	nfex	⊢ Ⅎ 𝑤 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
7	6	nfex	⊢ Ⅎ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
8		nfv	⊢ Ⅎ 𝑧 𝑣 = ⟨ 𝑥 , 𝑦 ⟩
9	8 2	nfan	⊢ Ⅎ 𝑧 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 )
10	9	nfex	⊢ Ⅎ 𝑧 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 )
11	10	nfex	⊢ Ⅎ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 )
12	3	anbi2d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
13	12	2exbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
14	7 11 13	cbvopab2	⊢ { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
15		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
16		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ 𝜓 } = { ⟨ 𝑣 , 𝑤 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
17	14 15 16	3eqtr4i	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ 𝜓 }