Metamath Proof Explorer

Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005) (Proof shortened by Wolf Lammen, 21-May-2025)

		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))$

Proof

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	1	2sbievw	$⊢ [z/ x] [w/ y] φ \leftrightarrow ψ$
4	3	anbi2i	$⊢ (φ \land [z/ x] [w/ y] φ) \leftrightarrow (φ \land ψ)$
5	4	imbi1i	$⊢ ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \leftrightarrow ((φ \land ψ) \to (x = z \land y = w))$
6	5	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))$
7	6	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))$
8	2 7	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))$