Theorem dfoprab2 7191

Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)

Assertion

Ref	Expression
dfoprab2	⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Distinct variable groups:   𝑥,𝑧,𝑤   𝑦,𝑧,𝑤   𝜑,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem dfoprab2

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		excom 2166	. . . 4 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
2		exrot4 2170	. . . . 5 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3		opeq1 4763	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ⟨𝑤, 𝑧⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
4	3	eqeq2d 2809	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑣 = ⟨𝑤, 𝑧⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
5	4	pm5.32ri 579	. . . . . . . . . 10 ⊢ ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
6	5	anbi1i 626	. . . . . . . . 9 ⊢ (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑))
7		anass 472	. . . . . . . . 9 ⊢ (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8		an32 645	. . . . . . . . 9 ⊢ (((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
9	6, 7, 8	3bitr3i 304	. . . . . . . 8 ⊢ ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
10	9	exbii 1849	. . . . . . 7 ⊢ (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
11		opex 5321	. . . . . . . . 9 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
12	11	isseti 3455	. . . . . . . 8 ⊢ ∃𝑤 𝑤 = ⟨𝑥, 𝑦⟩
13		19.42v 1954	. . . . . . . 8 ⊢ (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ ∃𝑤 𝑤 = ⟨𝑥, 𝑦⟩))
14	12, 13	mpbiran2 709	. . . . . . 7 ⊢ (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
15	10, 14	bitri 278	. . . . . 6 ⊢ (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
16	15	3exbii 1851	. . . . 5 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
17	2, 16	bitri 278	. . . 4 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
18		19.42vv 1958	. . . . 5 ⊢ (∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
19	18	2exbii 1850	. . . 4 ⊢ (∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20	1, 17, 19	3bitr3i 304	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
21	20	abbii 2863	. 2 ⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
22		df-oprab 7139	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
23		df-opab 5093	. 2 ⊢ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
24	21, 22, 23	3eqtr4i 2831	1 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781  {cab 2776  ⟨cop 4531  {copab 5092  {coprab 7136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-oprab 7139

This theorem is referenced by:  reloprab  7192  oprabv  7193  cbvoprab1  7220  cbvoprab12  7222  cbvoprab3  7224  dmoprab  7234  rnoprab  7236  ssoprab2i  7242  mpomptx  7244  resoprab  7249  funoprabg  7252  elrnmpores  7267  ov6g  7292  dfoprab3s  7733  xpcomco  8590  omxpenlem  8601  nvss  28376  mpomptxf  30442  bj-dfmpoa  34533  mpomptx2  44736