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

Theorem elin 3099
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
elin (A (B𝐶) ↔ (A B A 𝐶))

Proof of Theorem elin
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 elex 2539 . 2 (A (B𝐶) → A V)
2 elex 2539 . . 3 (A 𝐶A V)
32adantl 262 . 2 ((A B A 𝐶) → A V)
4 eleq1 2078 . . . 4 (x = A → (x BA B))
5 eleq1 2078 . . . 4 (x = A → (x 𝐶A 𝐶))
64, 5anbi12d 445 . . 3 (x = A → ((x B x 𝐶) ↔ (A B A 𝐶)))
7 df-in 2897 . . 3 (B𝐶) = {x ∣ (x B x 𝐶)}
86, 7elab2g 2662 . 2 (A V → (A (B𝐶) ↔ (A B A 𝐶)))
91, 3, 8pm5.21nii 607 1 (A (B𝐶) ↔ (A B A 𝐶))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1226   wcel 1370  Vcvv 2531  cin 2889
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-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-in 2897
This theorem is referenced by:  elin2  3100  elin3  3101  incom  3102  ineqri  3103  ineq1  3104  inass  3120  inss1  3130  ssin  3132  ssrin  3135  inssdif  3146  difin  3147  unssin  3149  inssun  3150  invdif  3152  indif  3153  indi  3157  undi  3158  difundi  3162  difindiss  3164  indifdir  3166  difin2  3172  inrab2  3183  inelcm  3255  inssdif0im  3264  uniin  3570  intun  3616  intpr  3617  elrint  3625  iunin2  3690  iinin2m  3695  elriin  3697  brin  3781  trin  3834  inex1  3861  inuni  3879  bnd2  3896  ordpwsucss  4223  ordpwsucexmid  4226  peano5  4244  inopab  4391  inxp  4393  dmin  4466  opelres  4540  intasym  4632  asymref  4633  dminss  4661  imainss  4662  inimasn  4664  ssrnres  4686  cnvresima  4733  dfco2a  4744  imainlem  4902  imain  4903  2elresin  4932  nfvres  5127  respreima  5216  isoini  5378  offval  5638  tfrlem5  5848  bdinex1  7261  peano5set  7301
  Copyright terms: Public domain W3C validator