Theorem dfint3 30705

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

Assertion

Ref	Expression
dfint3	|- |^| A = ( _V \ ( `' ( _V \ _E ) " A ) )

Proof of Theorem dfint3

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfint2 4251	. 2 |- |^| A = { x | A. y e. A x e. y }
2		ralnex 2869	. . . 4 |- ( A. y e. A -. y `' ( _V \ _E ) x <-> -. E. y e. A y `' ( _V \ _E ) x )
3		vex 3081	. . . . . . . . 9 |- y e. _V
4		vex 3081	. . . . . . . . 9 |- x e. _V
5	3, 4	brcnv 5029	. . . . . . . 8 |- ( y `' ( _V \ _E ) x <-> x ( _V \ _E ) y )
6		brv 30630	. . . . . . . . 9 |- x _V y
7		brdif 4468	. . . . . . . . 9 |- ( x ( _V \ _E ) y <-> ( x _V y /\ -. x _E y ) )
8	6, 7	mpbiran 926	. . . . . . . 8 |- ( x ( _V \ _E ) y <-> -. x _E y )
9	5, 8	bitr2i 253	. . . . . . 7 |- ( -. x _E y <-> y `' ( _V \ _E ) x )
10	9	con1bii 332	. . . . . 6 |- ( -. y `' ( _V \ _E ) x <-> x _E y )
11		epel 4760	. . . . . 6 |- ( x _E y <-> x e. y )
12	10, 11	bitr2i 253	. . . . 5 |- ( x e. y <-> -. y `' ( _V \ _E ) x )
13	12	ralbii 2854	. . . 4 |- ( A. y e. A x e. y <-> A. y e. A -. y `' ( _V \ _E ) x )
14		eldif 3443	. . . . . 6 |- ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> ( x e. _V /\ -. x e. ( `' ( _V \ _E ) " A ) ) )
15	4, 14	mpbiran 926	. . . . 5 |- ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> -. x e. ( `' ( _V \ _E ) " A ) )
16	4	elima 5185	. . . . 5 |- ( x e. ( `' ( _V \ _E ) " A ) <-> E. y e. A y `' ( _V \ _E ) x )
17	15, 16	xchbinx 311	. . . 4 |- ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> -. E. y e. A y `' ( _V \ _E ) x )
18	2, 13, 17	3bitr4ri 281	. . 3 |- ( x e. ( _V \ ( `' ( _V \ _E ) " A ) ) <-> A. y e. A x e. y )
19	18	abbi2i 2553	. 2 |- ( _V \ ( `' ( _V \ _E ) " A ) ) = { x | A. y e. A x e. y }
20	1, 19	eqtr4i 2452	1 |- |^| A = ( _V \ ( `' ( _V \ _E ) " A ) )

Syntax hints:   -. wn 3   = wceq 1437   e. wcel 1867   {cab 2405   A.wral 2773   E.wrex 2774   _Vcvv 3078   \ cdif 3430   |^|cint 4249   class class class wbr 4417   _E cep 4755   `'ccnv 4845   "cima 4849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-int 4250  df-br 4418  df-opab 4477  df-eprel 4757  df-xp 4852  df-cnv 4854  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859

This theorem is referenced by: (None)