Metamath Proof Explorer


Theorem dfint3

Description: Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018)

Ref Expression
Assertion dfint3 A=VVE-1A

Proof

Step Hyp Ref Expression
1 dfint2 A=x|yAxy
2 ralnex yA¬yVE-1x¬yAyVE-1x
3 vex yV
4 vex xV
5 3 4 brcnv yVE-1xxVEy
6 brv xVy
7 brdif xVEyxVy¬xEy
8 6 7 mpbiran xVEy¬xEy
9 5 8 bitr2i ¬xEyyVE-1x
10 9 con1bii ¬yVE-1xxEy
11 epel xEyxy
12 10 11 bitr2i xy¬yVE-1x
13 12 ralbii yAxyyA¬yVE-1x
14 eldif xVVE-1AxV¬xVE-1A
15 4 14 mpbiran xVVE-1A¬xVE-1A
16 4 elima xVE-1AyAyVE-1x
17 15 16 xchbinx xVVE-1A¬yAyVE-1x
18 2 13 17 3bitr4ri xVVE-1AyAxy
19 18 abbi2i VVE-1A=x|yAxy
20 1 19 eqtr4i A=VVE-1A