2sb5rf

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 distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		2sb5rf.1	$⊢ Ⅎ z φ$
2		2sb5rf.2	$⊢ Ⅎ w φ$
3	1	19.41	$⊢ \exists z (\exists w (z = x \land w = y) \land φ) \leftrightarrow (\exists z \exists w (z = x \land w = y) \land φ)$
4	2	19.41	$⊢ \exists w ((z = x \land w = y) \land φ) \leftrightarrow (\exists w (z = x \land w = y) \land φ)$
5	4	exbii	$⊢ \exists z \exists w ((z = x \land w = y) \land φ) \leftrightarrow \exists z (\exists w (z = x \land w = y) \land φ)$
6		2ax6e	$⊢ \exists z \exists w (z = x \land w = y)$
7	6	biantrur	$⊢ φ \leftrightarrow (\exists z \exists w (z = x \land w = y) \land φ)$
8	3 5 7	3bitr4ri	$⊢ φ \leftrightarrow \exists z \exists w ((z = x \land w = y) \land φ)$
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.32i	$⊢ ((z = x \land w = y) \land [z/ x] [w/ y] φ) \leftrightarrow ((z = x \land w = y) \land φ)$
13	12	2exbii	$⊢ \exists z \exists w ((z = x \land w = y) \land [z/ x] [w/ y] φ) \leftrightarrow \exists z \exists w ((z = x \land w = y) \land φ)$
14	8 13	bitr4i	$⊢ φ \leftrightarrow \exists z \exists w ((z = x \land w = y) \land [z/ x] [w/ y] φ)$

Metamath Proof Explorer

Theorem 2sb5rf

Proof