Theorem iinxprg 3496

Description: Indexed intersection with an unordered pair index.

Hypotheses

Ref	Expression
iinxprg.1	|- (x = A -> C = D)
iinxprg.2	|- (x = B -> C = E)

Assertion

Ref	Expression
iinxprg	|- ((A e. V /\ B e. W) -> |^|_x e. {A, B}C = (D i^i E))

Distinct variable groups:   x,A   x,B   x,D   x,E

Proof of Theorem iinxprg

Step	Hyp	Ref	Expression
1		ax-17 1605	. . . . 5 |- (y e. D -> A.x y e. D)
2		iinxprg.1	. . . . . 6 |- (x = A -> C = D)
3	2	eleq2d 2211	. . . . 5 |- (x = A -> (y e. C <-> y e. D))
4	1, 3	ceqsalg 2562	. . . 4 |- (A e. V -> (A.x(x = A -> y e. C) <-> y e. D))
5		ax-17 1605	. . . . 5 |- (y e. E -> A.x y e. E)
6		iinxprg.2	. . . . . 6 |- (x = B -> C = E)
7	6	eleq2d 2211	. . . . 5 |- (x = B -> (y e. C <-> y e. E))
8	5, 7	ceqsalg 2562	. . . 4 |- (B e. W -> (A.x(x = B -> y e. C) <-> y e. E))
9	4, 8	bi2anan9 950	. . 3 |- ((A e. V /\ B e. W) -> ((A.x(x = A -> y e. C) /\ A.x(x = B -> y e. C)) <-> (y e. D /\ y e. E)))
10		visset 2541	. . . . 5 |- y e. _V
11		eliin 3441	. . . . 5 |- (y e. _V -> (y e. |^|_x e. {A, B}C <-> A.x e. {A, B}y e. C))
12	10, 11	ax-mp 7	. . . 4 |- (y e. |^|_x e. {A, B}C <-> A.x e. {A, B}y e. C)
13		df-ral 2359	. . . 4 |- (A.x e. {A, B}y e. C <-> A.x(x e. {A, B} -> y e. C))
14		visset 2541	. . . . . . . . 9 |- x e. _V
15	14	elpr 3254	. . . . . . . 8 |- (x e. {A, B} <-> (x = A \/ x = B))
16	15	imbi1i 299	. . . . . . 7 |- ((x e. {A, B} -> y e. C) <-> ((x = A \/ x = B) -> y e. C))
17		jaob 822	. . . . . . 7 |- (((x = A \/ x = B) -> y e. C) <-> ((x = A -> y e. C) /\ (x = B -> y e. C)))
18	16, 17	bitri 279	. . . . . 6 |- ((x e. {A, B} -> y e. C) <-> ((x = A -> y e. C) /\ (x = B -> y e. C)))
19	18	albii 1635	. . . . 5 |- (A.x(x e. {A, B} -> y e. C) <-> A.x((x = A -> y e. C) /\ (x = B -> y e. C)))
20		19.26 1703	. . . . 5 |- (A.x((x = A -> y e. C) /\ (x = B -> y e. C)) <-> (A.x(x = A -> y e. C) /\ A.x(x = B -> y e. C)))
21	19, 20	bitri 279	. . . 4 |- (A.x(x e. {A, B} -> y e. C) <-> (A.x(x = A -> y e. C) /\ A.x(x = B -> y e. C)))
22	12, 13, 21	3bitri 289	. . 3 |- (y e. |^|_x e. {A, B}C <-> (A.x(x = A -> y e. C) /\ A.x(x = B -> y e. C)))
23		elin 2999	. . 3 |- (y e. (D i^i E) <-> (y e. D /\ y e. E))
24	9, 22, 23	3bitr4g 745	. 2 |- ((A e. V /\ B e. W) -> (y e. |^|_x e. {A, B}C <-> y e. (D i^i E)))
25	24	eqrdv 2139	1 |- ((A e. V /\ B e. W) -> |^|_x e. {A, B}C = (D i^i E))

Syntax hints:   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  A.wral 2355  _Vcvv 2538   i^i cin 2826  {cpr 3239  |^|_ciin 3437

This theorem is referenced by:  pmapmeet 18205

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-ral 2359  df-v 2540  df-un 2832  df-in 2834  df-sn 3242  df-pr 3243  df-iin 3439

Copyright terms: Public domain