Theorem opelxp 2452

Description: Ordered pair membership in a cross product.

Hypothesis

Ref	Expression
opelxp.1	⊢ B ∈ V

Assertion

Ref	Expression
opelxp	⊢ (⟨A, B⟩ ∈ (C × D) ↔ (A ∈ C ∧ B ∈ D))

Proof of Theorem opelxp

Step	Hyp	Ref	Expression
1		opelxpex 2445	. 2 ⊢ (⟨A, B⟩ ∈ (C × D) → A ∈ V)
2		elisset 1354	. . 3 ⊢ (A ∈ C → A ∈ V)
3	2	adantr 306	. 2 ⊢ ((A ∈ C ∧ B ∈ D) → A ∈ V)
4		opeq1 1876	. . . 4 ⊢ (z = A → ⟨z, B⟩ = ⟨A, B⟩)
5	4	eleq1d 1155	. . 3 ⊢ (z = A → (⟨z, B⟩ ∈ (C × D) ↔ ⟨A, B⟩ ∈ (C × D)))
6		eleq1 1149	. . . 4 ⊢ (z = A → (z ∈ C ↔ A ∈ C))
7	6	anbi1d 469	. . 3 ⊢ (z = A → ((z ∈ C ∧ B ∈ D) ↔ (A ∈ C ∧ B ∈ D)))
8		cleqcom 1103	. . . . . . . . . . 11 ⊢ (⟨z, B⟩ = ⟨x, y⟩ ↔ ⟨x, y⟩ = ⟨z, B⟩)
9		visset 1350	. . . . . . . . . . . 12 ⊢ x ∈ V
10		visset 1350	. . . . . . . . . . . 12 ⊢ y ∈ V
11		opelxp.1	. . . . . . . . . . . 12 ⊢ B ∈ V
12	9, 10, 11	opth 1898	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ = ⟨z, B⟩ ↔ (x = z ∧ y = B))
13	8, 12	bitr 151	. . . . . . . . . 10 ⊢ (⟨z, B⟩ = ⟨x, y⟩ ↔ (x = z ∧ y = B))
14	13	anbi1i 368	. . . . . . . . 9 ⊢ ((⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ ((x = z ∧ y = B) ∧ (x ∈ C ∧ y ∈ D)))
15		an4 388	. . . . . . . . 9 ⊢ (((x = z ∧ y = B) ∧ (x ∈ C ∧ y ∈ D)) ↔ ((x = z ∧ x ∈ C) ∧ (y = B ∧ y ∈ D)))
16	14, 15	bitr 151	. . . . . . . 8 ⊢ ((⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ ((x = z ∧ x ∈ C) ∧ (y = B ∧ y ∈ D)))
17	16	biex 733	. . . . . . 7 ⊢ (∃y(⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ ∃y((x = z ∧ x ∈ C) ∧ (y = B ∧ y ∈ D)))
18		19.42v 966	. . . . . . 7 ⊢ (∃y((x = z ∧ x ∈ C) ∧ (y = B ∧ y ∈ D)) ↔ ((x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
19	17, 18	bitr 151	. . . . . 6 ⊢ (∃y(⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ ((x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
20	19	biex 733	. . . . 5 ⊢ (∃x∃y(⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ ∃x((x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
21		19.41v 963	. . . . 5 ⊢ (∃x((x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)) ↔ (∃x(x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
22	20, 21	bitr 151	. . . 4 ⊢ (∃x∃y(⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)) ↔ (∃x(x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
23		elxp 2442	. . . 4 ⊢ (⟨z, B⟩ ∈ (C × D) ↔ ∃x∃y(⟨z, B⟩ = ⟨x, y⟩ ∧ (x ∈ C ∧ y ∈ D)))
24		df-clel 1099	. . . . 5 ⊢ (z ∈ C ↔ ∃x(x = z ∧ x ∈ C))
25		df-clel 1099	. . . . 5 ⊢ (B ∈ D ↔ ∃y(y = B ∧ y ∈ D))
26	24, 25	anbi12i 369	. . . 4 ⊢ ((z ∈ C ∧ B ∈ D) ↔ (∃x(x = z ∧ x ∈ C) ∧ ∃y(y = B ∧ y ∈ D)))
27	22, 23, 26	3bitr4 158	. . 3 ⊢ (⟨z, B⟩ ∈ (C × D) ↔ (z ∈ C ∧ B ∈ D))
28	5, 7, 27	vtoclbg 1384	. 2 ⊢ (A ∈ V → (⟨A, B⟩ ∈ (C × D) ↔ (A ∈ C ∧ B ∈ D)))
29	1, 3, 28	pm5.21nii 504	1 ⊢ (⟨A, B⟩ ∈ (C × D) ↔ (A ∈ C ∧ B ∈ D))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678   = weq 797   = wceq 1091   ∈ wcel 1092  Vcvv 1348  ⟨cop 1810   × cxp 2408

This theorem is referenced by:  brxp 2453  opelxpg 2454  ralxp 2456  opthprc 2457  elxp3 2460  optocl 2469  cbvop 2473  relsn 2485  ssxp 2487  xpex 2488  inxp 2496  opelres 2579  dfima2 2604  cnvxp 2651  relssdr 2668  opelf 2762  oprssdm 3056  df1st2 3098  brecop 3242  brecop2 3243  ecopoprdm 3245  eceqopreq 3249  xpdom2 3345  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  aceq5lem2 3559  ltpiord 3809  opelcn 4042  opelreal 4043  ruclem13 4897  infxpidmlem5 4937  infxpidmlem7 4939

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-opab 2098  df-xp 2424

metamath.org