Theorem eldif 3175

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 2783	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2783	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 276	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2268	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2268	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 669	. . . 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 3168	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2920	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 706	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   _Vcvv 2772   \ cdif 3163

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168

This theorem is referenced by:  eldifd  3176  eldifad  3177  eldifbd  3178  difeqri  3293  eldifi  3295  eldifn  3296  difdif  3298  ddifstab  3305  ssconb  3306  sscon  3307  ssdif  3308  raldifb  3313  dfss4st  3406  ssddif  3407  unssdif  3408  inssdif  3409  difin  3410  unssin  3412  inssun  3413  invdif  3415  indif  3416  difundi  3425  difindiss  3427  indifdir  3429  undif3ss  3434  difin2  3435  symdifxor  3439  dfnul2  3462  reldisj  3512  disj3  3513  undif4  3523  ssdif0im  3525  inssdif0im  3528  ssundifim  3544  eldifpr  3660  eldiftp  3679  eldifsn  3760  difprsnss  3771  iundif2ss  3993  iindif2m  3995  brdif  4098  unidif0  4212  eldifpw  4525  elirr  4590  en2lp  4603  difopab  4812  intirr  5070  cnvdif  5090  imadiflem  5354  imadif  5355  elfi2  7076  xrlenlt  8139  nzadd  9427  irradd  9769  irrmul  9770  fzdifsuc  10205  fisumss  11736  prodssdc  11933  fprodssdc  11934  bitscmp  12302  inffinp1  12833  bj-charfunr  15783