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	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ceqsralv2	$$⊢\forall x\in B\left(x=A\to \phi \right)\leftrightarrow \left(A\in B\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ceqsralv2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	notbid	$$⊢x=A\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	2	ceqsrexv2	$$⊢\exists x\in B\left(x=A\wedge \neg \phi \right)\leftrightarrow \left(A\in B\wedge \neg \psi \right)$$
4		rexanali	$$⊢\exists x\in B\left(x=A\wedge \neg \phi \right)\leftrightarrow \neg \forall x\in B\left(x=A\to \phi \right)$$
5		annim	$$⊢\left(A\in B\wedge \neg \psi \right)\leftrightarrow \neg \left(A\in B\to \psi \right)$$
6	3 4 5	3bitr3i	$$⊢\neg \forall x\in B\left(x=A\to \phi \right)\leftrightarrow \neg \left(A\in B\to \psi \right)$$
7	6	con4bii	$$⊢\forall x\in B\left(x=A\to \phi \right)\leftrightarrow \left(A\in B\to \psi \right)$$