Theorem eldif 3130

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 2741	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2741	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 274	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2233	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2233	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 662	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 470	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3123	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2877	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 699	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   _Vcvv 2730   \ cdif 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123

This theorem is referenced by:  eldifd  3131  eldifad  3132  eldifbd  3133  difeqri  3247  eldifi  3249  eldifn  3250  difdif  3252  ddifstab  3259  ssconb  3260  sscon  3261  ssdif  3262  raldifb  3267  dfss4st  3360  ssddif  3361  unssdif  3362  inssdif  3363  difin  3364  unssin  3366  inssun  3367  invdif  3369  indif  3370  difundi  3379  difindiss  3381  indifdir  3383  undif3ss  3388  difin2  3389  symdifxor  3393  dfnul2  3416  reldisj  3466  disj3  3467  undif4  3477  ssdif0im  3479  inssdif0im  3482  ssundifim  3498  eldifpr  3610  eldiftp  3629  eldifsn  3710  difprsnss  3718  iundif2ss  3938  iindif2m  3940  brdif  4042  unidif0  4153  eldifpw  4462  elirr  4525  en2lp  4538  difopab  4744  intirr  4997  cnvdif  5017  imadiflem  5277  imadif  5278  elfi2  6949  xrlenlt  7984  nzadd  9264  irradd  9605  irrmul  9606  fzdifsuc  10037  fisumss  11355  prodssdc  11552  fprodssdc  11553  inffinp1  12384  bj-charfunr  13845