Theorem iinrab2 4029

Description: Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)

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

Allowed substitution hints:   ph(x,y)

Proof of Theorem iinrab2

Step	Hyp	Ref	Expression
1		iineq1 3983	. . . . . 6 |- (A = (/) -> |^|_x e. A {y e. B | ph} = |^|_x e. (/) {y e. B | ph})
2		0iin 4024	. . . . . 6 |- |^|_x e. (/) {y e. B | ph} = _V
3	1, 2	syl6eq 2401	. . . . 5 |- (A = (/) -> |^|_x e. A {y e. B | ph} = _V)
4	3	ineq1d 3456	. . . 4 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = (_V i^i B))
5		incom 3448	. . . . 5 |- (_V i^i B) = (B i^i _V)
6		inv1 3577	. . . . 5 |- (B i^i _V) = B
7	5, 6	eqtri 2373	. . . 4 |- (_V i^i B) = B
8	4, 7	syl6eq 2401	. . 3 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = B)
9		rzal 3651	. . . 4 |- (A = (/) -> A.x e. A A.y e. B ph)
10		rabid2 2788	. . . . 5 |- (B = {y e. B | A.x e. A ph} <-> A.y e. B A.x e. A ph)
11		ralcom 2771	. . . . 5 |- (A.y e. B A.x e. A ph <-> A.x e. A A.y e. B ph)
12	10, 11	bitr2i 241	. . . 4 |- (A.x e. A A.y e. B ph <-> B = {y e. B | A.x e. A ph})
13	9, 12	sylib 188	. . 3 |- (A = (/) -> B = {y e. B | A.x e. A ph})
14	8, 13	eqtrd 2385	. 2 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph})
15		iinrab 4028	. . . 4 |- (A =/= (/) -> |^|_x e. A {y e. B | ph} = {y e. B | A.x e. A ph})
16	15	ineq1d 3456	. . 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 3351	. . . 4 |- {y e. B | A.x e. A ph} C_ B
18		dfss 3260	. . . 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 199	. . 3 |- {y e. B | A.x e. A ph} = ({y e. B | A.x e. A ph} i^i B)
20	16, 19	syl6eqr 2403	. 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 2592	1 |- (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph}

Syntax hints:   = wceq 1642   =/= wne 2516  A.wral 2614  {crab 2618  _Vcvv 2859   i^i cin 3208   C_ wss 3257  (/)c0 3550  |^|_ciin 3970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rab 2623  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-dif 3215  df-ss 3259  df-nul 3551  df-iin 3972

This theorem is referenced by: (None)