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

Metamath Proof Explorer

Theorem intab

Description: The intersection of a special case of a class abstraction. y may be free in ph and A , which can be thought of a ph ( y ) and A ( y ) . Typically, abrexex2 or abexssex can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006) (Proof shortened by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses intab.1 
|- A e. _V
intab.2 
|- { x | E. y ( ph /\ x = A ) } e. _V
Assertion intab 
|- |^| { x | A. y ( ph -> A e. x ) } = { x | E. y ( ph /\ x = A ) }

Proof

Step Hyp Ref Expression
1 intab.1 
 |-  A e. _V
2 intab.2 
 |-  { x | E. y ( ph /\ x = A ) } e. _V
3 eqeq1 
 |-  ( z = x -> ( z = A <-> x = A ) )
4 3 anbi2d 
 |-  ( z = x -> ( ( ph /\ z = A ) <-> ( ph /\ x = A ) ) )
5 4 exbidv 
 |-  ( z = x -> ( E. y ( ph /\ z = A ) <-> E. y ( ph /\ x = A ) ) )
6 5 cbvabv 
 |-  { z | E. y ( ph /\ z = A ) } = { x | E. y ( ph /\ x = A ) }
7 6 2 eqeltri 
 |-  { z | E. y ( ph /\ z = A ) } e. _V
8 nfe1 
 |-  F/ y E. y ( ph /\ z = A )
9 8 nfab 
 |-  F/_ y { z | E. y ( ph /\ z = A ) }
10 9 nfeq2 
 |-  F/ y x = { z | E. y ( ph /\ z = A ) }
11 eleq2 
 |-  ( x = { z | E. y ( ph /\ z = A ) } -> ( A e. x <-> A e. { z | E. y ( ph /\ z = A ) } ) )
12 11 imbi2d 
 |-  ( x = { z | E. y ( ph /\ z = A ) } -> ( ( ph -> A e. x ) <-> ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) ) )
13 10 12 albid 
 |-  ( x = { z | E. y ( ph /\ z = A ) } -> ( A. y ( ph -> A e. x ) <-> A. y ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) ) )
14 7 13 elab 
 |-  ( { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) } <-> A. y ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) )
15 19.8a 
 |-  ( ( ph /\ z = A ) -> E. y ( ph /\ z = A ) )
16 15 ex 
 |-  ( ph -> ( z = A -> E. y ( ph /\ z = A ) ) )
17 16 alrimiv 
 |-  ( ph -> A. z ( z = A -> E. y ( ph /\ z = A ) ) )
18 1 sbc6 
 |-  ( [. A / z ]. E. y ( ph /\ z = A ) <-> A. z ( z = A -> E. y ( ph /\ z = A ) ) )
19 17 18 sylibr 
 |-  ( ph -> [. A / z ]. E. y ( ph /\ z = A ) )
20 df-sbc 
 |-  ( [. A / z ]. E. y ( ph /\ z = A ) <-> A e. { z | E. y ( ph /\ z = A ) } )
21 19 20 sylib 
 |-  ( ph -> A e. { z | E. y ( ph /\ z = A ) } )
22 14 21 mpgbir 
 |-  { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) }
23 intss1 
 |-  ( { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) } -> |^| { x | A. y ( ph -> A e. x ) } C_ { z | E. y ( ph /\ z = A ) } )
24 22 23 ax-mp 
 |-  |^| { x | A. y ( ph -> A e. x ) } C_ { z | E. y ( ph /\ z = A ) }
25 19.29r 
 |-  ( ( E. y ( ph /\ z = A ) /\ A. y ( ph -> A e. x ) ) -> E. y ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) )
26 simplr 
 |-  ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z = A )
27 pm3.35 
 |-  ( ( ph /\ ( ph -> A e. x ) ) -> A e. x )
28 27 adantlr 
 |-  ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> A e. x )
29 26 28 eqeltrd 
 |-  ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z e. x )
30 29 exlimiv 
 |-  ( E. y ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z e. x )
31 25 30 syl 
 |-  ( ( E. y ( ph /\ z = A ) /\ A. y ( ph -> A e. x ) ) -> z e. x )
32 31 ex 
 |-  ( E. y ( ph /\ z = A ) -> ( A. y ( ph -> A e. x ) -> z e. x ) )
33 32 alrimiv 
 |-  ( E. y ( ph /\ z = A ) -> A. x ( A. y ( ph -> A e. x ) -> z e. x ) )
34 vex 
 |-  z e. _V
35 34 elintab 
 |-  ( z e. |^| { x | A. y ( ph -> A e. x ) } <-> A. x ( A. y ( ph -> A e. x ) -> z e. x ) )
36 33 35 sylibr 
 |-  ( E. y ( ph /\ z = A ) -> z e. |^| { x | A. y ( ph -> A e. x ) } )
37 36 abssi 
 |-  { z | E. y ( ph /\ z = A ) } C_ |^| { x | A. y ( ph -> A e. x ) }
38 24 37 eqssi 
 |-  |^| { x | A. y ( ph -> A e. x ) } = { z | E. y ( ph /\ z = A ) }
39 38 6 eqtri 
 |-  |^| { x | A. y ( ph -> A e. x ) } = { x | E. y ( ph /\ x = A ) }