2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005)

		Ref	Expression
	Hypothesis	2mos.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
	Assertion	2mos	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land ψ) \to (x = z \land y = w))$

Step	Hyp	Ref	Expression
1		2mos.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
2		2mo	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
3		nfv	$⊢ Ⅎ y x = z$
4	3	sbrim	$⊢ [w/ y] (x = z \to φ) \leftrightarrow (x = z \to [w/ y] φ)$
5	1	expcom	$⊢ y = w \to (x = z \to (φ \leftrightarrow ψ))$
6	5	pm5.74d	$⊢ y = w \to ((x = z \to φ) \leftrightarrow (x = z \to ψ))$
7	6	sbievw	$⊢ [w/ y] (x = z \to φ) \leftrightarrow (x = z \to ψ)$
8	4 7	bitr3i	$⊢ (x = z \to [w/ y] φ) \leftrightarrow (x = z \to ψ)$
9	8	pm5.74ri	$⊢ x = z \to ([w/ y] φ \leftrightarrow ψ)$
10	9	sbievw	$⊢ [z/ x] [w/ y] φ \leftrightarrow ψ$
11	10	anbi2i	$⊢ (φ \land [z/ x] [w/ y] φ) \leftrightarrow (φ \land ψ)$
12	11	imbi1i	$⊢ ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \leftrightarrow ((φ \land ψ) \to (x = z \land y = w))$
13	12	2albii	$⊢ \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \leftrightarrow \forall z \forall w ((φ \land ψ) \to (x = z \land y = w))$
14	13	2albii	$⊢ \forall x \forall y \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land ψ) \to (x = z \land y = w))$
15	2 14	bitri	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land ψ) \to (x = z \land y = w))$

Metamath Proof Explorer