opelopabsbALT

Description: The law of concretion in terms of substitutions. Less general than opelopabsb , but having a much shorter proof. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	opelopabsbALT	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow [w/ y] [z/ x] φ$

Proof

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists x (⟨z, w⟩ = ⟨x, y⟩ \land φ)$
2		vex	$⊢ z \in V$
3		vex	$⊢ w \in V$
4	2 3	opth	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \leftrightarrow (z = x \land w = y)$
5		equcom	$⊢ z = x \leftrightarrow x = z$
6		equcom	$⊢ w = y \leftrightarrow y = w$
7	5 6	anbi12ci	$⊢ (z = x \land w = y) \leftrightarrow (y = w \land x = z)$
8	4 7	bitri	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \leftrightarrow (y = w \land x = z)$
9	8	anbi1i	$⊢ (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ((y = w \land x = z) \land φ)$
10	9	2exbii	$⊢ \exists y \exists x (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists x ((y = w \land x = z) \land φ)$
11	1 10	bitri	$⊢ \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists x ((y = w \land x = z) \land φ)$
12		elopab	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ)$
13		2sb5	$⊢ [w/ y] [z/ x] φ \leftrightarrow \exists y \exists x ((y = w \land x = z) \land φ)$
14	11 12 13	3bitr4i	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow [w/ y] [z/ x] φ$

Metamath Proof Explorer

Theorem opelopabsbALT

Proof