Metamath Proof Explorer


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 )