Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

	Ref	Expression
Assertion	iinexg	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^|_ x e. A B e. _V )

Proof

Step	Hyp	Ref	Expression
1		dfiin2g	|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
2	1	adantl	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
3		elisset	|- ( B e. C -> E. y y = B )
4	3	rgenw	|- A. x e. A ( B e. C -> E. y y = B )
5		r19.2z	|- ( ( A =/= (/) /\ A. x e. A ( B e. C -> E. y y = B ) ) -> E. x e. A ( B e. C -> E. y y = B ) )
6	4 5	mpan2	|- ( A =/= (/) -> E. x e. A ( B e. C -> E. y y = B ) )
7		r19.35	|- ( E. x e. A ( B e. C -> E. y y = B ) <-> ( A. x e. A B e. C -> E. x e. A E. y y = B ) )
8	6 7	sylib	|- ( A =/= (/) -> ( A. x e. A B e. C -> E. x e. A E. y y = B ) )
9	8	imp	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> E. x e. A E. y y = B )
10		rexcom4	|- ( E. x e. A E. y y = B <-> E. y E. x e. A y = B )
11	9 10	sylib	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> E. y E. x e. A y = B )
12		abn0	|- ( { y | E. x e. A y = B } =/= (/) <-> E. y E. x e. A y = B )
13	11 12	sylibr	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> { y | E. x e. A y = B } =/= (/) )
14		intex	|- ( { y | E. x e. A y = B } =/= (/) <-> |^| { y | E. x e. A y = B } e. _V )
15	13 14	sylib	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^| { y | E. x e. A y = B } e. _V )
16	2 15	eqeltrd	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^|_ x e. A B e. _V )