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

Theorem eldif 2900
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif (A (B𝐶) ↔ (A B ¬ A 𝐶))

Proof of Theorem eldif
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 elex 2539 . 2 (A (B𝐶) → A V)
2 elex 2539 . . 3 (A BA V)
32adantr 261 . 2 ((A B ¬ A 𝐶) → A V)
4 eleq1 2078 . . . 4 (x = A → (x BA B))
5 eleq1 2078 . . . . 5 (x = A → (x 𝐶A 𝐶))
65notbid 579 . . . 4 (x = A → (¬ x 𝐶 ↔ ¬ A 𝐶))
74, 6anbi12d 445 . . 3 (x = A → ((x B ¬ x 𝐶) ↔ (A B ¬ A 𝐶)))
8 df-dif 2893 . . 3 (B𝐶) = {x ∣ (x B ¬ x 𝐶)}
97, 8elab2g 2662 . 2 (A V → (A (B𝐶) ↔ (A B ¬ A 𝐶)))
101, 3, 9pm5.21nii 607 1 (A (B𝐶) ↔ (A B ¬ A 𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   wa 97  wb 98   = wceq 1226   wcel 1370  Vcvv 2531  cdif 2887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-dif 2893
This theorem is referenced by:  eldifd  2901  eldifad  2902  eldifbd  2903  difeqri  3037  eldifi  3039  eldifn  3040  difdif  3042  ssconb  3049  sscon  3050  ssdif  3051  raldifb  3056  ssddif  3144  unssdif  3145  inssdif  3146  difin  3147  unssin  3149  inssun  3150  invdif  3152  indif  3153  difundi  3162  difindiss  3164  indifdir  3166  undif3ss  3171  difin2  3172  symdifxor  3176  dfnul2  3199  reldisj  3244  disj3  3245  undif4  3257  ssdif0im  3259  inssdif0im  3264  ssundifim  3279  eldifsn  3465  difprsnss  3472  iundif2ss  3692  iindif2m  3694  brdif  3782  unidif0  3890  eldifpw  4154  elirr  4204  en2lp  4212  difopab  4392  intirr  4634  cnvdif  4653  imadiflem  4900  imadif  4901  xrlenlt  6679
  Copyright terms: Public domain W3C validator