This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )