2sb6

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

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

Step	Hyp	Ref	Expression
1		sb6	$⊢ [z/ x] [w/ y] φ \leftrightarrow \forall x (x = z \to [w/ y] φ)$
2		19.21v	$⊢ \forall y (x = z \to (y = w \to φ)) \leftrightarrow (x = z \to \forall y (y = w \to φ))$
3		impexp	$⊢ ((x = z \land y = w) \to φ) \leftrightarrow (x = z \to (y = w \to φ))$
4	3	albii	$⊢ \forall y ((x = z \land y = w) \to φ) \leftrightarrow \forall y (x = z \to (y = w \to φ))$
5		sb6	$⊢ [w/ y] φ \leftrightarrow \forall y (y = w \to φ)$
6	5	imbi2i	$⊢ (x = z \to [w/ y] φ) \leftrightarrow (x = z \to \forall y (y = w \to φ))$
7	2 4 6	3bitr4ri	$⊢ (x = z \to [w/ y] φ) \leftrightarrow \forall y ((x = z \land y = w) \to φ)$
8	7	albii	$⊢ \forall x (x = z \to [w/ y] φ) \leftrightarrow \forall x \forall y ((x = z \land y = w) \to φ)$
9	1 8	bitri	$⊢ [z/ x] [w/ y] φ \leftrightarrow \forall x \forall y ((x = z \land y = w) \to φ)$

Metamath Proof Explorer