ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eldif GIF version

Theorem eldif 3130
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.
StepHypRef Expression
1 elex 2741 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2741 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 274 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2233 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2233 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 662 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 470 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 3123 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 2877 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 699 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104   = wceq 1348  wcel 2141  Vcvv 2730  cdif 3118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123
This theorem is referenced by:  eldifd  3131  eldifad  3132  eldifbd  3133  difeqri  3247  eldifi  3249  eldifn  3250  difdif  3252  ddifstab  3259  ssconb  3260  sscon  3261  ssdif  3262  raldifb  3267  dfss4st  3360  ssddif  3361  unssdif  3362  inssdif  3363  difin  3364  unssin  3366  inssun  3367  invdif  3369  indif  3370  difundi  3379  difindiss  3381  indifdir  3383  undif3ss  3388  difin2  3389  symdifxor  3393  dfnul2  3416  reldisj  3466  disj3  3467  undif4  3477  ssdif0im  3479  inssdif0im  3482  ssundifim  3498  eldifpr  3610  eldiftp  3629  eldifsn  3710  difprsnss  3718  iundif2ss  3938  iindif2m  3940  brdif  4042  unidif0  4153  eldifpw  4462  elirr  4525  en2lp  4538  difopab  4744  intirr  4997  cnvdif  5017  imadiflem  5277  imadif  5278  elfi2  6949  xrlenlt  7984  nzadd  9264  irradd  9605  irrmul  9606  fzdifsuc  10037  fisumss  11355  prodssdc  11552  fprodssdc  11553  inffinp1  12384  bj-charfunr  13845
  Copyright terms: Public domain W3C validator