Theorem ceqsralv

Description: Restricted quantifier version of ceqsalv . (Contributed by NM, 21-Jun-2013) Avoid ax-9 , ax-12 , ax-ext . (Revised by SN, 8-Sep-2024)

	Ref	Expression
Hypothesis	ceqsralv.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ceqsralv	$$⊢A\in B\to \left(\forall x\in B\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ceqsralv.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	pm5.74i	$$⊢\left(x=A\to \phi \right)\leftrightarrow \left(x=A\to \psi \right)$$
3	2	ralbii	$$⊢\forall x\in B\left(x=A\to \phi \right)\leftrightarrow \forall x\in B\left(x=A\to \psi \right)$$
4		r19.23v	$$⊢\forall x\in B\left(x=A\to \psi \right)\leftrightarrow \left(\exists x\in Bx=A\to \psi \right)$$
5		risset	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$
6		pm5.5	$$⊢\exists x\in Bx=A\to \left(\left(\exists x\in Bx=A\to \psi \right)\leftrightarrow \psi \right)$$
7	5 6	sylbi	$$⊢A\in B\to \left(\left(\exists x\in Bx=A\to \psi \right)\leftrightarrow \psi \right)$$
8	4 7	bitrid	$$⊢A\in B\to \left(\forall x\in B\left(x=A\to \psi \right)\leftrightarrow \psi \right)$$
9	3 8	bitrid	$$⊢A\in B\to \left(\forall x\in B\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$