Theorem riotaeqdv

Description: Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Hypothesis	riotaeqdv.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	riotaeqdv	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		riotaeqdv.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
3	2	anbi1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
4	3	iotabidv	⊢ ( 𝜑 → ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
5		df-riota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
6		df-riota	⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
7	4 5 6	3eqtr4g	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )