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 | |
|
intab.2 | |
||
Assertion | intab | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intab.1 | |
|
2 | intab.2 | |
|
3 | eqeq1 | |
|
4 | 3 | anbi2d | |
5 | 4 | exbidv | |
6 | 5 | cbvabv | |
7 | 6 2 | eqeltri | |
8 | nfe1 | |
|
9 | 8 | nfab | |
10 | 9 | nfeq2 | |
11 | eleq2 | |
|
12 | 11 | imbi2d | |
13 | 10 12 | albid | |
14 | 7 13 | elab | |
15 | 19.8a | |
|
16 | 15 | ex | |
17 | 16 | alrimiv | |
18 | 1 | sbc6 | |
19 | 17 18 | sylibr | |
20 | df-sbc | |
|
21 | 19 20 | sylib | |
22 | 14 21 | mpgbir | |
23 | intss1 | |
|
24 | 22 23 | ax-mp | |
25 | 19.29r | |
|
26 | simplr | |
|
27 | pm3.35 | |
|
28 | 27 | adantlr | |
29 | 26 28 | eqeltrd | |
30 | 29 | exlimiv | |
31 | 25 30 | syl | |
32 | 31 | ex | |
33 | 32 | alrimiv | |
34 | vex | |
|
35 | 34 | elintab | |
36 | 33 35 | sylibr | |
37 | 36 | abssi | |
38 | 24 37 | eqssi | |
39 | 38 6 | eqtri | |