Theorem resoprab 4067

Description: Restriction of an operation class abstraction.

Assertion

Ref	Expression
resoprab	⊢ ({⟨⟨x, y⟩, z⟩∣φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ φ)}

Distinct variable groups:   x,y,z,A   x,B,y,z

Proof of Theorem resoprab

Step	Hyp	Ref	Expression
1		resopab 3452	. . 3 ⊢ ({⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)} ↾ (A × B)) = {⟨w, z⟩∣(w ∈ (A × B) ⋀ ∃x∃y(w = ⟨x, y⟩ ⋀ φ))}
2		19.42vv 1352	. . . . 5 ⊢ (∃x∃y(w ∈ (A × B) ⋀ (w = ⟨x, y⟩ ⋀ φ)) ↔ (w ∈ (A × B) ⋀ ∃x∃y(w = ⟨x, y⟩ ⋀ φ)))
3		an12 495	. . . . . . 7 ⊢ ((w ∈ (A × B) ⋀ (w = ⟨x, y⟩ ⋀ φ)) ↔ (w = ⟨x, y⟩ ⋀ (w ∈ (A × B) ⋀ φ)))
4		eleq1 1581	. . . . . . . . . 10 ⊢ (w = ⟨x, y⟩ → (w ∈ (A × B) ↔ ⟨x, y⟩ ∈ (A × B)))
5		visset 1860	. . . . . . . . . . 11 ⊢ y ∈ V
6	5	opelxp 3271	. . . . . . . . . 10 ⊢ (⟨x, y⟩ ∈ (A × B) ↔ (x ∈ A ⋀ y ∈ B))
7	4, 6	syl6bb 547	. . . . . . . . 9 ⊢ (w = ⟨x, y⟩ → (w ∈ (A × B) ↔ (x ∈ A ⋀ y ∈ B)))
8	7	anbi1d 628	. . . . . . . 8 ⊢ (w = ⟨x, y⟩ → ((w ∈ (A × B) ⋀ φ) ↔ ((x ∈ A ⋀ y ∈ B) ⋀ φ)))
9	8	pm5.32i 656	. . . . . . 7 ⊢ ((w = ⟨x, y⟩ ⋀ (w ∈ (A × B) ⋀ φ)) ↔ (w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ)))
10	3, 9	bitri 180	. . . . . 6 ⊢ ((w ∈ (A × B) ⋀ (w = ⟨x, y⟩ ⋀ φ)) ↔ (w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ)))
11	10	2exbii 1093	. . . . 5 ⊢ (∃x∃y(w ∈ (A × B) ⋀ (w = ⟨x, y⟩ ⋀ φ)) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ)))
12	2, 11	bitr3i 182	. . . 4 ⊢ ((w ∈ (A × B) ⋀ ∃x∃y(w = ⟨x, y⟩ ⋀ φ)) ↔ ∃x∃y(w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ)))
13	12	opabbii 2726	. . 3 ⊢ {⟨w, z⟩∣(w ∈ (A × B) ⋀ ∃x∃y(w = ⟨x, y⟩ ⋀ φ))} = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ))}
14	1, 13	eqtri 1542	. 2 ⊢ ({⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)} ↾ (A × B)) = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ))}
15		dfoprab2 4049	. . 3 ⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)}
16		reseq1 3425	. . 3 ⊢ ({⟨⟨x, y⟩, z⟩∣φ} = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)} → ({⟨⟨x, y⟩, z⟩∣φ} ↾ (A × B)) = ({⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)} ↾ (A × B)))
17	15, 16	ax-mp 7	. 2 ⊢ ({⟨⟨x, y⟩, z⟩∣φ} ↾ (A × B)) = ({⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ φ)} ↾ (A × B))
18		dfoprab2 4049	. 2 ⊢ {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ φ)} = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ⋀ ((x ∈ A ⋀ y ∈ B) ⋀ φ))}
19	14, 17, 18	3eqtr4i 1552	1 ⊢ ({⟨⟨x, y⟩, z⟩∣φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ φ)}

Syntax hints:   ⋀ wa 230   = wceq 997   ∈ wcel 999  ∃wex 1021  ⟨cop 2463  {copab 2721   × cxp 3225   ↾ cres 3229  {copab2 4022

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-opab 2722  df-xp 3241  df-rel 3242  df-res 3247  df-oprab 4024

Copyright terms: Public domain