Theorem sbciegftOLD

Description: Obsolete version of sbciegft as of 14-May-2025. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbciegftOLD	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbc5	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(x=A\wedge \phi \right)$$
2		biimp	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\phi \to \psi \right)$$
3	2	imim2i	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(x=A\to \left(\phi \to \psi \right)\right)$$
4	3	impd	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(x=A\wedge \phi \right)\to \psi \right)$$
5	4	alimi	$$⊢\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \forall x\left(\left(x=A\wedge \phi \right)\to \psi \right)$$
6		19.23t	$$⊢Ⅎx\psi \to \left(\forall x\left(\left(x=A\wedge \phi \right)\to \psi \right)\leftrightarrow \left(\exists x\left(x=A\wedge \phi \right)\to \psi \right)\right)$$
7	6	biimpa	$$⊢\left(Ⅎx\psi \wedge \forall x\left(\left(x=A\wedge \phi \right)\to \psi \right)\right)\to \left(\exists x\left(x=A\wedge \phi \right)\to \psi \right)$$
8	5 7	sylan2	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\exists x\left(x=A\wedge \phi \right)\to \psi \right)$$
9	8	3adant1	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\exists x\left(x=A\wedge \phi \right)\to \psi \right)$$
10	1 9	biimtrid	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \psi \right)$$
11		biimpr	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\psi \to \phi \right)$$
12	11	imim2i	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(x=A\to \left(\psi \to \phi \right)\right)$$
13	12	com23	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\psi \to \left(x=A\to \phi \right)\right)$$
14	13	alimi	$$⊢\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \forall x\left(\psi \to \left(x=A\to \phi \right)\right)$$
15		19.21t	$$⊢Ⅎx\psi \to \left(\forall x\left(\psi \to \left(x=A\to \phi \right)\right)\leftrightarrow \left(\psi \to \forall x\left(x=A\to \phi \right)\right)\right)$$
16	15	biimpa	$$⊢\left(Ⅎx\psi \wedge \forall x\left(\psi \to \left(x=A\to \phi \right)\right)\right)\to \left(\psi \to \forall x\left(x=A\to \phi \right)\right)$$
17	14 16	sylan2	$$⊢\left(Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\psi \to \forall x\left(x=A\to \phi \right)\right)$$
18	17	3adant1	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\psi \to \forall x\left(x=A\to \phi \right)\right)$$
19		sbc6g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
20	19	3ad2ant1	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
21	18 20	sylibrd	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
22	10 21	impbid	$$⊢\left(A\in V\wedge Ⅎx\psi \wedge \forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$