Theorem riotabiia

Description: Equivalent wff's yield equal restricted iotas (inference form). ( rabbiia analog.) (Contributed by NM, 16-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		riotabiia.1	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		eqid	⊢ V = V
3	1	adantl	⊢ ( ( V = V ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
4	3	riotabidva	⊢ ( V = V → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐴 𝜓 ) )
5	2 4	ax-mp	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ∈ 𝐴 𝜓 )