Theorem dfoprab2 7425

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 2168	. . . 4 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
2		exrot4 2172	. . . . 5 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3		opeq1 4816	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ⟨𝑤, 𝑧⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
4	3	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑣 = ⟨𝑤, 𝑧⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
5	4	pm5.32ri 575	. . . . . . . . . 10 ⊢ ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
6	5	anbi1i 625	. . . . . . . . 9 ⊢ (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑))
7		anass 468	. . . . . . . . 9 ⊢ (((𝑣 = ⟨𝑤, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
8		an32 647	. . . . . . . . 9 ⊢ (((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ∧ 𝜑) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
9	6, 7, 8	3bitr3i 301	. . . . . . . 8 ⊢ ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
10	9	exbii 1850	. . . . . . 7 ⊢ (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩))
11		opex 5416	. . . . . . . . 9 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
12	11	isseti 3447	. . . . . . . 8 ⊢ ∃𝑤 𝑤 = ⟨𝑥, 𝑦⟩
13		19.42v 1955	. . . . . . . 8 ⊢ (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ ∃𝑤 𝑤 = ⟨𝑥, 𝑦⟩))
14	12, 13	mpbiran2 711	. . . . . . 7 ⊢ (∃𝑤((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ∧ 𝑤 = ⟨𝑥, 𝑦⟩) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
15	10, 14	bitri 275	. . . . . 6 ⊢ (∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
16	15	3exbii 1852	. . . . 5 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
17	2, 16	bitri 275	. . . 4 ⊢ (∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
18		19.42vv 1959	. . . . 5 ⊢ (∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
19	18	2exbii 1851	. . . 4 ⊢ (∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = ⟨𝑤, 𝑧⟩ ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20	1, 17, 19	3bitr3i 301	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
21	20	abbii 2803	. 2 ⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
22		df-oprab 7371	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
23		df-opab 5148	. 2 ⊢ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))}
24	21, 22, 23	3eqtr4i 2769	1 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781  {cab 2714  ⟨cop 4573  {copab 5147  {coprab 7368

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-oprab 7371

This theorem is referenced by:  reloprab  7426  oprabv  7427  cbvoprab1  7454  cbvoprab12  7456  cbvoprab3  7458  dmoprab  7470  rnoprab  7472  ssoprab2i  7478  mpomptx  7480  resoprab  7485  funoprabg  7488  elrnmpores  7505  ov6g  7531  dfoprab3s  8006  xpcomco  9005  omxpenlem  9016  nvss  30664  mpomptxf  32751  bj-dfmpoa  37430  mpomptx2  48811