Theorem cnvopab 6135

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 2178, ax-12 2215. (Revised by SN, 7-Jun-2025.)

Assertion

Ref	Expression
cnvopab	⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem cnvopab

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relcnv 6104	. 2 ⊢ Rel ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2		relopabv 5806	. 2 ⊢ Rel {⟨𝑦, 𝑥⟩ ∣ 𝜑}
3		elopab 5509	. . . 4 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
4		excom 2199	. . . 4 ⊢ (∃𝑥∃𝑦(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑥(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5		ancom 466	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))
6		vex 3457	. . . . . . . 8 ⊢ 𝑤 ∈ V
7		vex 3457	. . . . . . . 8 ⊢ 𝑧 ∈ V
8	6, 7	opth 5456	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦))
9	7, 6	opth 5456	. . . . . . 7 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))
10	5, 8, 9	3bitr4i 306	. . . . . 6 ⊢ (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩)
11	10	anbi1i 636	. . . . 5 ⊢ ((⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
12	11	2exbii 1882	. . . 4 ⊢ (∃𝑦∃𝑥(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
13	3, 4, 12	3bitri 300	. . 3 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
14	7, 6	opelcnv 5865	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
15		elopab 5509	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ 𝜑} ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
16	13, 14, 15	3bitr4i 306	. 2 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ 𝜑})
17	1, 2, 16	eqrelriiv 5774	1 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4593  {copab 5171  ^◡ccnv 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667

This theorem is used by:  mptcnv  6136  cnvxpOLD  6153  mptpreima  6238  f1ocnvd  7668  cnvoprab  8060  mapsncnv  8903  cnvepnep  9590  compsscnv  10376  dfiso2  17865  xkocnv  24041  lgsquadlem3  27616  axcontlem2  29408  cnvadj  32359  f1o3d  33086  vxp  38998  xrninxp  39150  prjspeclsp  43445  fsovrfovd  44836