Metamath Proof Explorer

Theorem sb7fALT

Description: Alternate version of sb7f . (Contributed by NM, 26-Jul-2006) (Revised by Mario Carneiro, 6-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dfsb1.p9	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		sb7fALT.1	$⊢ Ⅎ z φ$
	Assertion	sb7fALT	$⊢ θ \leftrightarrow \exists z (z = y \land \exists x (x = z \land φ))$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.p9	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		sb7fALT.1	$⊢ Ⅎ z φ$
3		biid	$⊢ ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ)))) \leftrightarrow ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ))))$
4		biid	$⊢ ((z = y \to \exists x (x = z \land φ)) \land \exists z (z = y \land \exists x (x = z \land φ))) \leftrightarrow ((z = y \to \exists x (x = z \land φ)) \land \exists z (z = y \land \exists x (x = z \land φ)))$
5		biid	$⊢ ((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow ((x = z \to φ) \land \exists x (x = z \land φ))$
6	5 2	sb5fALT	$⊢ ((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow \exists x (x = z \land φ)$
7	3 4 6	sbbiiALT	$⊢ ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ)))) \leftrightarrow ((z = y \to \exists x (x = z \land φ)) \land \exists z (z = y \land \exists x (x = z \land φ)))$
8	1 3 2	sbco2ALT	$⊢ ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ)))) \leftrightarrow θ$
9	4	sb5ALT2	$⊢ ((z = y \to \exists x (x = z \land φ)) \land \exists z (z = y \land \exists x (x = z \land φ))) \leftrightarrow \exists z (z = y \land \exists x (x = z \land φ))$
10	7 8 9	3bitr3i	$⊢ θ \leftrightarrow \exists z (z = y \land \exists x (x = z \land φ))$