Theorem iotabii

Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypothesis	iotabii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	iotabii	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		iotabii.1	⊢ ( 𝜑 ↔ 𝜓 )
2		iotabi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑥 𝜓 ) )
3	2 1	mpg	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑥 𝜓 )