Theorem ralbinrald

Description: Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017)

	Ref	Expression
Hypotheses	ralbinrald.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	ralbinrald.2	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 = 𝑋 )
	ralbinrald.3	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜃 ) )
Assertion	ralbinrald	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		ralbinrald.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2		ralbinrald.2	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 = 𝑋 )
3		ralbinrald.3	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜃 ) )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝜓 ↔ 𝜃 ) )
5	1 4	rspcdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → 𝜃 ) )
6	3	bicomd	⊢ ( 𝑥 = 𝑋 → ( 𝜃 ↔ 𝜓 ) )
7	2 6	syl	⊢ ( 𝑥 ∈ 𝐴 → ( 𝜃 ↔ 𝜓 ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜃 ↔ 𝜓 ) )
9	8	biimpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜃 → 𝜓 ) )
10	9	ralrimdva	⊢ ( 𝜑 → ( 𝜃 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )
11	5 10	impbid	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ 𝜃 ) )