2sb5

Description: Equivalence for double substitution. (Contributed by NM, 3-Feb-2005)

		Ref	Expression
	Assertion	2sb5	$⊢ [z/ x] [w/ y] φ \leftrightarrow \exists x \exists y ((x = z \land y = w) \land φ)$

Step	Hyp	Ref	Expression
1		sb5	$⊢ [z/ x] [w/ y] φ \leftrightarrow \exists x (x = z \land [w/ y] φ)$
2		19.42v	$⊢ \exists y (x = z \land (y = w \land φ)) \leftrightarrow (x = z \land \exists y (y = w \land φ))$
3		anass	$⊢ ((x = z \land y = w) \land φ) \leftrightarrow (x = z \land (y = w \land φ))$
4	3	exbii	$⊢ \exists y ((x = z \land y = w) \land φ) \leftrightarrow \exists y (x = z \land (y = w \land φ))$
5		sb5	$⊢ [w/ y] φ \leftrightarrow \exists y (y = w \land φ)$
6	5	anbi2i	$⊢ (x = z \land [w/ y] φ) \leftrightarrow (x = z \land \exists y (y = w \land φ))$
7	2 4 6	3bitr4ri	$⊢ (x = z \land [w/ y] φ) \leftrightarrow \exists y ((x = z \land y = w) \land φ)$
8	7	exbii	$⊢ \exists x (x = z \land [w/ y] φ) \leftrightarrow \exists x \exists y ((x = z \land y = w) \land φ)$
9	1 8	bitri	$⊢ [z/ x] [w/ y] φ \leftrightarrow \exists x \exists y ((x = z \land y = w) \land φ)$

Metamath Proof Explorer