Theorem eldif 3209

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 2814	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2814	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 276	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2294	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2294	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 673	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 473	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3202	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2953	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 711	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1397   e. wcel 2202   _Vcvv 2802   \ cdif 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202

This theorem is referenced by:  eldifd  3210  eldifad  3211  eldifbd  3212  difeqri  3327  eldifi  3329  eldifn  3330  difdif  3332  ddifstab  3339  ssconb  3340  sscon  3341  ssdif  3342  raldifb  3347  dfss4st  3440  ssddif  3441  unssdif  3442  inssdif  3443  difin  3444  unssin  3446  inssun  3447  invdif  3449  indif  3450  difundi  3459  difindiss  3461  indifdir  3463  undif3ss  3468  difin2  3469  symdifxor  3473  dfnul2  3496  reldisj  3546  disj3  3547  undif4  3557  ssdif0im  3559  inssdif0im  3562  ssundifim  3578  eldifpr  3696  eldiftp  3715  eldifsn  3800  difprsnss  3811  iundif2ss  4036  iindif2m  4038  brdif  4142  unidif0  4257  eldifpw  4574  elirr  4639  en2lp  4652  difopab  4863  intirr  5123  cnvdif  5143  imadiflem  5409  imadif  5410  elfi2  7170  xrlenlt  8243  nzadd  9531  irradd  9879  irrmul  9880  fzdifsuc  10315  fisumss  11952  prodssdc  12149  fprodssdc  12150  bitscmp  12518  inffinp1  13049  bj-charfunr  16405