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 ) " A ) )

Proof

Step Hyp Ref Expression
1 dfint2
 |-  |^| A = { x | A. y e. A x e. y }
2 ralnex
 |-  ( A. y e. A -. y `' ( _V \ _E ) x <-> -. E. y e. A y `' ( _V \ _E ) x )
3 vex
 |-  y e. _V
4 vex
 |-  x e. _V
5 3 4 brcnv
 |-  ( y `' ( _V \ _E ) 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 ) x )
10 9 con1bii
 |-  ( -. y `' ( _V \ _E ) x <-> x _E y )
11 epel
 |-  ( x _E y <-> x e. y )
12 10 11 bitr2i
 |-  ( x e. y <-> -. y `' ( _V \ _E ) x )
13 12 ralbii
 |-  ( A. y e. A x e. y <-> A. y e. A -. y `' ( _V \ _E ) x )
14 eldif
 |-  ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> ( x e. _V /\ -. x e. ( `' ( _V \ _E ) " A ) ) )
15 4 14 mpbiran
 |-  ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> -. x e. ( `' ( _V \ _E ) " A ) )
16 4 elima
 |-  ( x e. ( `' ( _V \ _E ) " A ) <-> E. y e. A y `' ( _V \ _E ) x )
17 15 16 xchbinx
 |-  ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> -. E. y e. A y `' ( _V \ _E ) x )
18 2 13 17 3bitr4ri
 |-  ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> A. y e. A x e. y )
19 18 abbi2i
 |-  ( _V \ ( `' ( _V \ _E ) " A ) ) = { x | A. y e. A x e. y }
20 1 19 eqtr4i
 |-  |^| A = ( _V \ ( `' ( _V \ _E ) " A ) )