Theorem eldif 3223

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 2827	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2827	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 276	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2297	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2297	. . . . 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 3216	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2967	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 712	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2205   _Vcvv 2815   \ cdif 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-dif 3216

This theorem is referenced by:  eldifd  3224  eldifad  3225  eldifbd  3226  difeqri  3343  eldifi  3345  eldifn  3346  difdif  3348  ddifstab  3355  ssconb  3356  sscon  3357  ssdif  3358  raldifb  3363  dfss4st  3458  ssddif  3459  unssdif  3460  inssdif  3461  difin  3462  unssin  3464  inssun  3465  invdif  3467  indif  3468  difundi  3477  difindiss  3479  indifdir  3481  undif3ss  3486  difin2  3487  symdifxor  3491  dfnul2  3514  reldisj  3564  disj3  3565  undif4  3575  ssdif0im  3577  inssdif0im  3580  ssundifim  3597  eldifpr  3721  eldiftp  3740  eldifsn  3825  difprsnss  3837  iundif2ss  4062  iindif2m  4064  brdif  4168  unidif0  4285  eldifpw  4603  elirr  4668  en2lp  4681  difopab  4893  intirr  5154  cnvdif  5174  imadiflem  5440  imadif  5441  suppimacnvfn  6459  suppssdc  6473  suppssrst  6474  suppssrgst  6475  elfi2  7272  xrlenlt  8354  nzadd  9647  irradd  9996  irrmul  9997  fzdifsuc  10437  fisumss  12103  prodssdc  12300  fprodssdc  12301  bitscmp  12669  ballotfilemdifcfi  13169  ballotfilemdifcfz  13171  ballotfilemodife  13184  ballotfilemth  13225  inffinp1  13264  bj-charfunr  16706