cbvoprab2

Description: Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 11-Dec-2016)

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

Proof

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

Metamath Proof Explorer

Theorem cbvoprab2

Proof