Theorem iinrab2 3319

Description: Indexed intersection of a restricted class builder.

Assertion

Ref	Expression
iinrab2	|- (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph}

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

Proof of Theorem iinrab2

Step	Hyp	Ref	Expression
1		iineq1 3270	. . . . . 6 |- (A = (/) -> |^|_x e. A {y e. B | ph} = |^|_x e. (/) {y e. B | ph})
2		0iin 3313	. . . . . 6 |- |^|_x e. (/) {y e. B | ph} = _V
3	1, 2	syl6eq 1944	. . . . 5 |- (A = (/) -> |^|_x e. A {y e. B | ph} = _V)
4	3	ineq1d 2795	. . . 4 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = (_V i^i B))
5		incom 2787	. . . . 5 |- (_V i^i B) = (B i^i _V)
6		inv1 2898	. . . . 5 |- (B i^i _V) = B
7	5, 6	eqtri 1908	. . . 4 |- (_V i^i B) = B
8	4, 7	syl6eq 1944	. . 3 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = B)
9		rzal 2970	. . . 4 |- (A = (/) -> A.x e. A A.y e. B ph)
10		rabid2 2254	. . . . 5 |- (B = {y e. B | A.x e. A ph} <-> A.y e. B A.x e. A ph)
11		ralcom 2242	. . . . 5 |- (A.y e. B A.x e. A ph <-> A.x e. A A.y e. B ph)
12	10, 11	bitr2i 191	. . . 4 |- (A.x e. A A.y e. B ph <-> B = {y e. B | A.x e. A ph})
13	9, 12	sylib 215	. . 3 |- (A = (/) -> B = {y e. B | A.x e. A ph})
14	8, 13	eqtrd 1925	. 2 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph})
15		iinrab 3318	. . . 4 |- (A =/= (/) -> |^|_x e. A {y e. B | ph} = {y e. B | A.x e. A ph})
16	15	ineq1d 2795	. . 3 |- (A =/= (/) -> (|^|_x e. A {y e. B | ph} i^i B) = ({y e. B | A.x e. A ph} i^i B))
17		ssrab2 2692	. . . 4 |- {y e. B | A.x e. A ph} C_ B
18		dfss 2606	. . . 4 |- ({y e. B | A.x e. A ph} C_ B <-> {y e. B | A.x e. A ph} = ({y e. B | A.x e. A ph} i^i B))
19	17, 18	mpbi 206	. . 3 |- {y e. B | A.x e. A ph} = ({y e. B | A.x e. A ph} i^i B)
20	16, 19	syl6eqr 1946	. 2 |- (A =/= (/) -> (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph})
21	14, 20	pm2.61ine 2089	1 |- (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph}

Syntax hints:   = wceq 1298   =/= wne 2017  A.wral 2105  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  |^|_ciin 3256

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rab 2112  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876  df-iin 3258

Copyright terms: Public domain