Theorem cnvopab 6141

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 2183, ax-12 2220. (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 6110	. 2 ⊢ Rel ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2		relopabv 5812	. 2 ⊢ Rel {⟨𝑦, 𝑥⟩ ∣ 𝜑}
3		elopab 5515	. . . 4 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
4		excom 2204	. . . 4 ⊢ (∃𝑥∃𝑦(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑥(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5		ancom 465	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))
6		vex 3466	. . . . . . . 8 ⊢ 𝑤 ∈ V
7		vex 3466	. . . . . . . 8 ⊢ 𝑧 ∈ V
8	6, 7	opth 5462	. . . . . . 7 ⊢ (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦))
9	7, 6	opth 5462	. . . . . . 7 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))
10	5, 8, 9	3bitr4i 306	. . . . . 6 ⊢ (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩)
11	10	anbi1i 635	. . . . 5 ⊢ ((⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
12	11	2exbii 1877	. . . 4 ⊢ (∃𝑦∃𝑥(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
13	3, 4, 12	3bitri 300	. . 3 ⊢ (⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
14	7, 6	opelcnv 5871	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑤, 𝑧⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
15		elopab 5515	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ 𝜑} ↔ ∃𝑦∃𝑥(⟨𝑧, 𝑤⟩ = ⟨𝑦, 𝑥⟩ ∧ 𝜑))
16	13, 14, 15	3bitr4i 306	. 2 ⊢ (⟨𝑧, 𝑤⟩ ∈ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑦, 𝑥⟩ ∣ 𝜑})
17	1, 2, 16	eqrelriiv 5780	1 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}

Syntax hints:   ∧ wa 400   = wceq 1568  ∃wex 1807   ∈ wcel 2150  ⟨cop 4600  {copab 5178  ^◡ccnv 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-11 2199  ax-ext 2742  ax-sep 5262  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5671  df-rel 5672  df-cnv 5673

This theorem is referenced by:  mptcnv  6142  cnvxp  6158  mptpreima  6243  f1ocnvd  7665  cnvoprab  8060  mapsncnv  8894  cnvepnep  9580  compsscnv  10358  dfiso2  17832  xkocnv  23954  lgsquadlem3  27526  axcontlem2  29285  cnvadj  32214  f1o3d  32941  vxp  38862  xrninxp  39014  prjspeclsp  43296  fsovrfovd  44687