Theorem eldif 3222

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 3215	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2966	. 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 3210

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 3215

This theorem is referenced by:  eldifd  3223  eldifad  3224  eldifbd  3225  difeqri  3341  eldifi  3343  eldifn  3344  difdif  3346  ddifstab  3353  ssconb  3354  sscon  3355  ssdif  3356  raldifb  3361  dfss4st  3456  ssddif  3457  unssdif  3458  inssdif  3459  difin  3460  unssin  3462  inssun  3463  invdif  3465  indif  3466  difundi  3475  difindiss  3477  indifdir  3479  undif3ss  3484  difin2  3485  symdifxor  3489  dfnul2  3512  reldisj  3562  disj3  3563  undif4  3573  ssdif0im  3575  inssdif0im  3578  ssundifim  3595  eldifpr  3718  eldiftp  3737  eldifsn  3822  difprsnss  3834  iundif2ss  4059  iindif2m  4061  brdif  4165  unidif0  4282  eldifpw  4600  elirr  4665  en2lp  4678  difopab  4890  intirr  5151  cnvdif  5171  imadiflem  5437  imadif  5438  suppimacnvfn  6448  suppssdc  6462  suppssrst  6463  suppssrgst  6464  elfi2  7261  xrlenlt  8340  nzadd  9632  irradd  9981  irrmul  9982  fzdifsuc  10419  fisumss  12082  prodssdc  12279  fprodssdc  12280  bitscmp  12648  ballotfilemdifcfi  13148  ballotfilemodife  13158  inffinp1  13197  bj-charfunr  16597