Theorem eldif 3229

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 2833	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 2833	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 276	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2301	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 677	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 477	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3222	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2973	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 716	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∖ cdif 3217

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222

This theorem is referenced by:  eldifd  3230  eldifad  3231  eldifbd  3232  difeqri  3349  eldifi  3351  eldifn  3352  difdif  3354  ddifstab  3361  ssconb  3362  sscon  3363  ssdif  3364  raldifb  3369  dfss4st  3464  ssddif  3465  unssdif  3466  inssdif  3467  difin  3468  unssin  3470  inssun  3471  invdif  3473  indif  3474  difundi  3483  difindiss  3485  indifdir  3487  undif3ss  3492  difin2  3493  symdifxor  3497  reldisj  3575  disj3  3576  undif4  3586  ssdif0im  3588  inssdif0im  3591  ssundifim  3608  eldifpr  3732  eldiftp  3751  eldifsn  3836  difprsnss  3848  iundif2ss  4073  iindif2m  4075  brdif  4179  unidif0  4299  eldifpw  4618  elirr  4683  en2lp  4696  difopab  4908  intirr  5169  cnvdif  5189  imadiflem  5455  imadif  5456  suppimacnvfn  6476  suppssdc  6490  suppssrst  6491  suppssrgst  6492  elfi2  7296  xrlenlt  8380  nzadd  9676  irradd  10025  irrmul  10026  fzdifsuc  10466  fisumss  12137  prodssdc  12334  fprodssdc  12335  bitscmp  12703  ballotfilemdifcfi  13203  ballotfilemdifcfz  13205  ballotfilemodife  13218  ballotfilemth  13259  inffinp1  13298  bj-charfunr  16750