Theorem eldif 3030

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
eldif	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Proof of Theorem eldif

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2652	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2652	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 272	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2162	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2162	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 633	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 460	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3023	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2784	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 661	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 103   <-> wb 104   = wceq 1299   e. wcel 1448   _Vcvv 2641   \ cdif 3018

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-dif 3023

This theorem is referenced by:  eldifd  3031  eldifad  3032  eldifbd  3033  difeqri  3143  eldifi  3145  eldifn  3146  difdif  3148  ddifstab  3155  ssconb  3156  sscon  3157  ssdif  3158  raldifb  3163  dfss4st  3256  ssddif  3257  unssdif  3258  inssdif  3259  difin  3260  unssin  3262  inssun  3263  invdif  3265  indif  3266  difundi  3275  difindiss  3277  indifdir  3279  undif3ss  3284  difin2  3285  symdifxor  3289  dfnul2  3312  reldisj  3361  disj3  3362  undif4  3372  ssdif0im  3374  inssdif0im  3377  ssundifim  3393  eldifsn  3597  difprsnss  3605  iundif2ss  3825  iindif2m  3827  brdif  3923  unidif0  4031  eldifpw  4336  elirr  4394  en2lp  4407  difopab  4610  intirr  4861  cnvdif  4881  imadiflem  5138  imadif  5139  xrlenlt  7701  nzadd  8958  irradd  9288  irrmul  9289  fzdifsuc  9702  fisumss  11000  inffinp1  11734