Theorem bj-ceqsalt

Description: Remove from ceqsalt dependency on ax-ext (and on df-cleq and df-v ). Note: this is not doable with ceqsralt (or ceqsralv ), which uses eleq1 , but the same dependence removal is possible for ceqsalg , ceqsal , ceqsalv , cgsexg , cgsex2g , cgsex4g , ceqsex , ceqsexv , ceqsex2 , ceqsex2v , ceqsex3v , ceqsex4v , ceqsex6v , ceqsex8v , gencbvex (after changing A = y to y = A ), gencbvex2 , gencbval , vtoclgft (it uses F/_ , whose justification nfcjust does not use ax-ext ) and several other vtocl* theorems (see for instance bj-vtoclg1f ). See also bj-ceqsaltv . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ceqsalt	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge A\in V\right)\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-elisset	$$⊢A\in V\to \exists xx=A$$
2	1	3anim3i	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge A\in V\right)\to \left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \exists xx=A\right)$$
3		bj-ceqsalt0	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \exists xx=A\right)\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$
4	2 3	syl	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge A\in V\right)\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$