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 AV
intab.2 x|yφx=AV
Assertion intab x|yφAx=x|yφx=A

Proof

Step Hyp Ref Expression
1 intab.1 AV
2 intab.2 x|yφx=AV
3 eqeq1 z=xz=Ax=A
4 3 anbi2d z=xφz=Aφx=A
5 4 exbidv z=xyφz=Ayφx=A
6 5 cbvabv z|yφz=A=x|yφx=A
7 6 2 eqeltri z|yφz=AV
8 nfe1 yyφz=A
9 8 nfab _yz|yφz=A
10 9 nfeq2 yx=z|yφz=A
11 eleq2 x=z|yφz=AAxAz|yφz=A
12 11 imbi2d x=z|yφz=AφAxφAz|yφz=A
13 10 12 albid x=z|yφz=AyφAxyφAz|yφz=A
14 7 13 elab z|yφz=Ax|yφAxyφAz|yφz=A
15 19.8a φz=Ayφz=A
16 15 ex φz=Ayφz=A
17 16 alrimiv φzz=Ayφz=A
18 1 sbc6 [˙A/z]˙yφz=Azz=Ayφz=A
19 17 18 sylibr φ[˙A/z]˙yφz=A
20 df-sbc [˙A/z]˙yφz=AAz|yφz=A
21 19 20 sylib φAz|yφz=A
22 14 21 mpgbir z|yφz=Ax|yφAx
23 intss1 z|yφz=Ax|yφAxx|yφAxz|yφz=A
24 22 23 ax-mp x|yφAxz|yφz=A
25 19.29r yφz=AyφAxyφz=AφAx
26 simplr φz=AφAxz=A
27 pm3.35 φφAxAx
28 27 adantlr φz=AφAxAx
29 26 28 eqeltrd φz=AφAxzx
30 29 exlimiv yφz=AφAxzx
31 25 30 syl yφz=AyφAxzx
32 31 ex yφz=AyφAxzx
33 32 alrimiv yφz=AxyφAxzx
34 vex zV
35 34 elintab zx|yφAxxyφAxzx
36 33 35 sylibr yφz=Azx|yφAx
37 36 abssi z|yφz=Ax|yφAx
38 24 37 eqssi x|yφAx=z|yφz=A
39 38 6 eqtri x|yφAx=x|yφx=A