This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabi 
 |-  ( _V \ ( `' ( _V \ _E ) " A ) ) = { x | A. y e. A x e. y }
20 1 19 eqtr4i 
 |-  |^| A = ( _V \ ( `' ( _V \ _E ) " A ) )