Metamath Proof Explorer


Theorem dfint3

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

Ref Expression
Assertion dfint3 A = V V E -1 A

Proof

Step Hyp Ref Expression
1 dfint2 A = x | y A x y
2 ralnex y A ¬ y V E -1 x ¬ y A y V E -1 x
3 vex y V
4 vex x V
5 3 4 brcnv y V E -1 x x V E y
6 brv x V y
7 brdif x V E y x V y ¬ x E y
8 6 7 mpbiran x V E y ¬ x E y
9 5 8 bitr2i ¬ x E y y V E -1 x
10 9 con1bii ¬ y V E -1 x x E y
11 epel x E y x y
12 10 11 bitr2i x y ¬ y V E -1 x
13 12 ralbii y A x y y A ¬ y V E -1 x
14 eldif x V V E -1 A x V ¬ x V E -1 A
15 4 14 mpbiran x V V E -1 A ¬ x V E -1 A
16 4 elima x V E -1 A y A y V E -1 x
17 15 16 xchbinx x V V E -1 A ¬ y A y V E -1 x
18 2 13 17 3bitr4ri x V V E -1 A y A x y
19 18 abbi2i V V E -1 A = x | y A x y
20 1 19 eqtr4i A = V V E -1 A