Theorem sbralieALT

Description: Alternative shorter proof of sbralie dependent on ax-ext , df-cleq , df-clel . (Contributed by NM, 5-Sep-2004) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	sbralie.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	sbralieALT	$$⊢\forall x\in y\phi \leftrightarrow \left[y/x\right]\forall y\in x\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbralie.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		cbvralsvw	$$⊢\forall y\in x\psi \leftrightarrow \forall z\in x\left[z/y\right]\psi$$
3	2	sbbii	$$⊢\left[y/x\right]\forall y\in x\psi \leftrightarrow \left[y/x\right]\forall z\in x\left[z/y\right]\psi$$
4		raleq	$$⊢x=y\to \left(\forall z\in x\left[z/y\right]\psi \leftrightarrow \forall z\in y\left[z/y\right]\psi \right)$$
5	4	sbievw	$$⊢\left[y/x\right]\forall z\in x\left[z/y\right]\psi \leftrightarrow \forall z\in y\left[z/y\right]\psi$$
6		cbvralsvw	$$⊢\forall z\in y\left[z/y\right]\psi \leftrightarrow \forall x\in y\left[x/z\right]\left[z/y\right]\psi$$
7		sbco2vv	$$⊢\left[x/z\right]\left[z/y\right]\psi \leftrightarrow \left[x/y\right]\psi$$
8	1	bicomd	$$⊢x=y\to \left(\psi \leftrightarrow \phi \right)$$
9	8	equcoms	$$⊢y=x\to \left(\psi \leftrightarrow \phi \right)$$
10	9	sbievw	$$⊢\left[x/y\right]\psi \leftrightarrow \phi$$
11	7 10	bitri	$$⊢\left[x/z\right]\left[z/y\right]\psi \leftrightarrow \phi$$
12	11	ralbii	$$⊢\forall x\in y\left[x/z\right]\left[z/y\right]\psi \leftrightarrow \forall x\in y\phi$$
13	6 12	bitri	$$⊢\forall z\in y\left[z/y\right]\psi \leftrightarrow \forall x\in y\phi$$
14	3 5 13	3bitrri	$$⊢\forall x\in y\phi \leftrightarrow \left[y/x\right]\forall y\in x\psi$$