Theorem iinrab2 4030

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 3984	. . . . . 6 |- (A = (/) -> |^|_x e. A {y e. B | ph} = |^|_x e. (/) {y e. B | ph})
2		0iin 4025	. . . . . 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 3457	. . . 4 |- (A = (/) -> (|^|_x e. A {y e. B | ph} i^i B) = (_V i^i B))
5		incom 3449	. . . . 5 |- (_V i^i B) = (B i^i _V)
6		inv1 3578	. . . . 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 3652	. . . 4 |- (A = (/) -> A.x e. A A.y e. B ph)
10		rabid2 2789	. . . . 5 |- (B = {y e. B | A.x e. A ph} <-> A.y e. B A.x e. A ph)
11		ralcom 2772	. . . . 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 4029	. . . 4 |- (A =/= (/) -> |^|_x e. A {y e. B | ph} = {y e. B | A.x e. A ph})
16	15	ineq1d 3457	. . 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 3352	. . . 4 |- {y e. B | A.x e. A ph} C_ B
18		dfss 3261	. . . 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 2593	1 |- (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph}

Syntax hints:   = wceq 1642   =/= wne 2517  A.wral 2615  {crab 2619  _Vcvv 2860   i^i cin 3209   C_ wss 3258  (/)c0 3551  |^|_ciin 3971

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 2479  df-ne 2519  df-ral 2620  df-rab 2624  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-dif 3216  df-ss 3260  df-nul 3552  df-iin 3973

This theorem is referenced by: (None)