Theorem eldif 3206

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
eldif	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Proof of Theorem eldif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2811	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 2811	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 276	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2292	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2292	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 671	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 473	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3199	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2950	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 709	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ 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  3794  difprsnss  3805  iundif2ss  4030  iindif2m  4032  brdif  4136  unidif0  4250  eldifpw  4567  elirr  4632  en2lp  4645  difopab  4854  intirr  5114  cnvdif  5134  imadiflem  5399  imadif  5400  elfi2  7135  xrlenlt  8207  nzadd  9495  irradd  9837  irrmul  9838  fzdifsuc  10273  fisumss  11898  prodssdc  12095  fprodssdc  12096  bitscmp  12464  inffinp1  12995  bj-charfunr  16131