Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

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

Proof

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