Metamath Proof Explorer

Theorem sbbiALT

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

		Ref	Expression
	Hypotheses	dfsb1.p6	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		dfsb1.s4	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
		dfsb1.bi	$⊢ η \leftrightarrow ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
	Assertion	sbbiALT	$⊢ η \leftrightarrow (θ \leftrightarrow τ)$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.p6	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		dfsb1.s4	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
3		dfsb1.bi	$⊢ η \leftrightarrow ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
4		biid	$⊢ ((x = y \to ((φ \to ψ) \land (ψ \to φ))) \land \exists x (x = y \land ((φ \to ψ) \land (ψ \to φ)))) \leftrightarrow ((x = y \to ((φ \to ψ) \land (ψ \to φ))) \land \exists x (x = y \land ((φ \to ψ) \land (ψ \to φ))))$
5		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
6	3 4 5	sbbiiALT	$⊢ η \leftrightarrow ((x = y \to ((φ \to ψ) \land (ψ \to φ))) \land \exists x (x = y \land ((φ \to ψ) \land (ψ \to φ))))$
7		biid	$⊢ ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
8	1 2 7	sbimALT	$⊢ ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \leftrightarrow (θ \to τ)$
9		biid	$⊢ ((x = y \to (ψ \to φ)) \land \exists x (x = y \land (ψ \to φ))) \leftrightarrow ((x = y \to (ψ \to φ)) \land \exists x (x = y \land (ψ \to φ)))$
10	2 1 9	sbimALT	$⊢ ((x = y \to (ψ \to φ)) \land \exists x (x = y \land (ψ \to φ))) \leftrightarrow (τ \to θ)$
11	8 10	anbi12i	$⊢ (((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \land ((x = y \to (ψ \to φ)) \land \exists x (x = y \land (ψ \to φ)))) \leftrightarrow ((θ \to τ) \land (τ \to θ))$
12	7 9 4	sbanALT	$⊢ ((x = y \to ((φ \to ψ) \land (ψ \to φ))) \land \exists x (x = y \land ((φ \to ψ) \land (ψ \to φ)))) \leftrightarrow (((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \land ((x = y \to (ψ \to φ)) \land \exists x (x = y \land (ψ \to φ))))$
13		dfbi2	$⊢ (θ \leftrightarrow τ) \leftrightarrow ((θ \to τ) \land (τ \to θ))$
14	11 12 13	3bitr4i	$⊢ ((x = y \to ((φ \to ψ) \land (ψ \to φ))) \land \exists x (x = y \land ((φ \to ψ) \land (ψ \to φ)))) \leftrightarrow (θ \leftrightarrow τ)$
15	6 14	bitri	$⊢ η \leftrightarrow (θ \leftrightarrow τ)$