Theorem sbbiiALT

Description: Alternate version of sbbii . (Contributed by NM, 14-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dfsb1.ph	$$⊢\theta \leftrightarrow \left(\left(x=y\to \phi \right)\wedge \exists x\left(x=y\wedge \phi \right)\right)$$
	dfsb1.ps	$$⊢\tau \leftrightarrow \left(\left(x=y\to \psi \right)\wedge \exists x\left(x=y\wedge \psi \right)\right)$$
	sbbiiALT.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	sbbiiALT	$$⊢\theta \leftrightarrow \tau$$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.ph	$$⊢\theta \leftrightarrow \left(\left(x=y\to \phi \right)\wedge \exists x\left(x=y\wedge \phi \right)\right)$$
2		dfsb1.ps	$$⊢\tau \leftrightarrow \left(\left(x=y\to \psi \right)\wedge \exists x\left(x=y\wedge \psi \right)\right)$$
3		sbbiiALT.1	$$⊢\phi \leftrightarrow \psi$$
4	3	biimpi	$$⊢\phi \to \psi$$
5	1 2 4	sbimiALT	$$⊢\theta \to \tau$$
6	3	biimpri	$$⊢\psi \to \phi$$
7	2 1 6	sbimiALT	$$⊢\tau \to \theta$$
8	5 7	impbii	$$⊢\theta \leftrightarrow \tau$$