2sb6rf

Description: Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Feb-2005) (Revised by Mario Carneiro, 6-Oct-2016) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (Proof shortened by Wolf Lammen, 13-Apr-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2sb5rf.1	$⊢ Ⅎ z φ$
	2sb5rf.2	$⊢ Ⅎ w φ$
Assertion	2sb6rf	$⊢ φ \leftrightarrow \forall z \forall w ((z = x \land w = y) \to [z/ x] [w/ y] φ)$

Proof

Step	Hyp	Ref	Expression
1		2sb5rf.1	$⊢ Ⅎ z φ$
2		2sb5rf.2	$⊢ Ⅎ w φ$
3	1	19.23	$⊢ \forall z (\exists w (z = x \land w = y) \to φ) \leftrightarrow (\exists z \exists w (z = x \land w = y) \to φ)$
4	2	19.23	$⊢ \forall w ((z = x \land w = y) \to φ) \leftrightarrow (\exists w (z = x \land w = y) \to φ)$
5	4	albii	$⊢ \forall z \forall w ((z = x \land w = y) \to φ) \leftrightarrow \forall z (\exists w (z = x \land w = y) \to φ)$
6		2ax6e	$⊢ \exists z \exists w (z = x \land w = y)$
7	6	a1bi	$⊢ φ \leftrightarrow (\exists z \exists w (z = x \land w = y) \to φ)$
8	3 5 7	3bitr4ri	$⊢ φ \leftrightarrow \forall z \forall w ((z = x \land w = y) \to φ)$
9		sbequ12r	$⊢ z = x \to ([z/ x] [w/ y] φ \leftrightarrow [w/ y] φ)$
10		sbequ12r	$⊢ w = y \to ([w/ y] φ \leftrightarrow φ)$
11	9 10	sylan9bb	$⊢ (z = x \land w = y) \to ([z/ x] [w/ y] φ \leftrightarrow φ)$
12	11	pm5.74i	$⊢ ((z = x \land w = y) \to [z/ x] [w/ y] φ) \leftrightarrow ((z = x \land w = y) \to φ)$
13	12	2albii	$⊢ \forall z \forall w ((z = x \land w = y) \to [z/ x] [w/ y] φ) \leftrightarrow \forall z \forall w ((z = x \land w = y) \to φ)$
14	8 13	bitr4i	$⊢ φ \leftrightarrow \forall z \forall w ((z = x \land w = y) \to [z/ x] [w/ y] φ)$

Metamath Proof Explorer

Theorem 2sb6rf

Proof