This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvopab

Description: The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-12 . (Revised by SN, 7-Jun-2025)

		Ref	Expression
	Assertion	cnvopab	$⊢ {\{⟨x, y⟩ \| φ\}}^{-1} = \{⟨y, x⟩ \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel {\{⟨x, y⟩ \| φ\}}^{-1}$
2		relopabv	$⊢ Rel \{⟨y, x⟩ \| φ\}$
3		elopab	$⊢ ⟨w, z⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (⟨w, z⟩ = ⟨x, y⟩ \land φ)$
4		excom	$⊢ \exists x \exists y (⟨w, z⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists x (⟨w, z⟩ = ⟨x, y⟩ \land φ)$
5		ancom	$⊢ (w = x \land z = y) \leftrightarrow (z = y \land w = x)$
6		vex	$⊢ w \in V$
7		vex	$⊢ z \in V$
8	6 7	opth	$⊢ ⟨w, z⟩ = ⟨x, y⟩ \leftrightarrow (w = x \land z = y)$
9	7 6	opth	$⊢ ⟨z, w⟩ = ⟨y, x⟩ \leftrightarrow (z = y \land w = x)$
10	5 8 9	3bitr4i	$⊢ ⟨w, z⟩ = ⟨x, y⟩ \leftrightarrow ⟨z, w⟩ = ⟨y, x⟩$
11	10	anbi1i	$⊢ (⟨w, z⟩ = ⟨x, y⟩ \land φ) \leftrightarrow (⟨z, w⟩ = ⟨y, x⟩ \land φ)$
12	11	2exbii	$⊢ \exists y \exists x (⟨w, z⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists x (⟨z, w⟩ = ⟨y, x⟩ \land φ)$
13	3 4 12	3bitri	$⊢ ⟨w, z⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists y \exists x (⟨z, w⟩ = ⟨y, x⟩ \land φ)$
14	7 6	opelcnv	$⊢ ⟨z, w⟩ \in {\{⟨x, y⟩ \| φ\}}^{-1} \leftrightarrow ⟨w, z⟩ \in \{⟨x, y⟩ \| φ\}$
15		elopab	$⊢ ⟨z, w⟩ \in \{⟨y, x⟩ \| φ\} \leftrightarrow \exists y \exists x (⟨z, w⟩ = ⟨y, x⟩ \land φ)$
16	13 14 15	3bitr4i	$⊢ ⟨z, w⟩ \in {\{⟨x, y⟩ \| φ\}}^{-1} \leftrightarrow ⟨z, w⟩ \in \{⟨y, x⟩ \| φ\}$
17	1 2 16	eqrelriiv	$⊢ {\{⟨x, y⟩ \| φ\}}^{-1} = \{⟨y, x⟩ \| φ\}$