Theorem ceqsralv2

Description: Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020)

	Ref	Expression
Hypothesis	ceqsralv2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	ceqsralv2	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ceqsralv2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2	1	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3	2	ceqsrexv2	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ ¬ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝜓 ) )
4		rexanali	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) )
5		annim	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝐴 ∈ 𝐵 → 𝜓 ) )
6	3 4 5	3bitr3i	⊢ ( ¬ ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ¬ ( 𝐴 ∈ 𝐵 → 𝜓 ) )
7	6	con4bii	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) )