Theorem eldif 3206

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 2811	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2811	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 276	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2292	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2292	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 671	. . . 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 3199	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2950	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 709	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   _Vcvv 2799   \ cdif 3194

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199

This theorem is referenced by:  eldifd  3207  eldifad  3208  eldifbd  3209  difeqri  3324  eldifi  3326  eldifn  3327  difdif  3329  ddifstab  3336  ssconb  3337  sscon  3338  ssdif  3339  raldifb  3344  dfss4st  3437  ssddif  3438  unssdif  3439  inssdif  3440  difin  3441  unssin  3443  inssun  3444  invdif  3446  indif  3447  difundi  3456  difindiss  3458  indifdir  3460  undif3ss  3465  difin2  3466  symdifxor  3470  dfnul2  3493  reldisj  3543  disj3  3544  undif4  3554  ssdif0im  3556  inssdif0im  3559  ssundifim  3575  eldifpr  3693  eldiftp  3712  eldifsn  3795  difprsnss  3806  iundif2ss  4031  iindif2m  4033  brdif  4137  unidif0  4251  eldifpw  4568  elirr  4633  en2lp  4646  difopab  4855  intirr  5115  cnvdif  5135  imadiflem  5400  imadif  5401  elfi2  7139  xrlenlt  8211  nzadd  9499  irradd  9841  irrmul  9842  fzdifsuc  10277  fisumss  11903  prodssdc  12100  fprodssdc  12101  bitscmp  12469  inffinp1  13000  bj-charfunr  16173