Theorem eldif 2997

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 2624	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2624	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 270	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2147	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2147	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 625	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 457	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 2990	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2753	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 653	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 102   <-> wb 103   = wceq 1287   e. wcel 1436   _Vcvv 2615   \ cdif 2985

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-dif 2990

This theorem is referenced by:  eldifd  2998  eldifad  2999  eldifbd  3000  difeqri  3109  eldifi  3111  eldifn  3112  difdif  3114  ddifstab  3121  ssconb  3122  sscon  3123  ssdif  3124  raldifb  3129  dfss4st  3221  ssddif  3222  unssdif  3223  inssdif  3224  difin  3225  unssin  3227  inssun  3228  invdif  3230  indif  3231  difundi  3240  difindiss  3242  indifdir  3244  undif3ss  3249  difin2  3250  symdifxor  3254  dfnul2  3277  reldisj  3322  disj3  3323  undif4  3333  ssdif0im  3335  inssdif0im  3338  ssundifim  3353  eldifsn  3549  difprsnss  3557  iundif2ss  3777  iindif2m  3779  brdif  3867  unidif0  3975  eldifpw  4270  elirr  4328  en2lp  4341  difopab  4535  intirr  4781  cnvdif  4800  imadiflem  5054  imadif  5055  xrlenlt  7487  nzadd  8727  irradd  9055  irrmul  9056  fzdifsuc  9417