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

Theorem elin 3120
 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 2560 . 2 (A (B𝐶) → A V)
2 elex 2560 . . 3 (A 𝐶A V)
32adantl 262 . 2 ((A B A 𝐶) → A V)
4 eleq1 2097 . . . 4 (x = A → (x BA B))
5 eleq1 2097 . . . 4 (x = A → (x 𝐶A 𝐶))
64, 5anbi12d 442 . . 3 (x = A → ((x B x 𝐶) ↔ (A B A 𝐶)))
7 df-in 2918 . . 3 (B𝐶) = {x ∣ (x B x 𝐶)}
86, 7elab2g 2683 . 2 (A V → (A (B𝐶) ↔ (A B A 𝐶)))
91, 3, 8pm5.21nii 619 1 (A (B𝐶) ↔ (A B A 𝐶))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1242   ∈ wcel 1390  Vcvv 2551   ∩ cin 2910 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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-in 2918 This theorem is referenced by:  elin2  3121  elin3  3122  incom  3123  ineqri  3124  ineq1  3125  inass  3141  inss1  3151  ssin  3153  ssrin  3156  inssdif  3167  difin  3168  unssin  3170  inssun  3171  invdif  3173  indif  3174  indi  3178  undi  3179  difundi  3183  difindiss  3185  indifdir  3187  difin2  3193  inrab2  3204  inelcm  3276  inssdif0im  3285  uniin  3591  intun  3637  intpr  3638  elrint  3646  iunin2  3711  iinin2m  3716  elriin  3718  brin  3802  trin  3855  inex1  3882  inuni  3900  bnd2  3917  ordpwsucss  4243  ordpwsucexmid  4246  peano5  4264  inopab  4411  inxp  4413  dmin  4486  opelres  4560  intasym  4652  asymref  4653  dminss  4681  imainss  4682  inimasn  4684  ssrnres  4706  cnvresima  4753  dfco2a  4764  imainlem  4923  imain  4924  2elresin  4953  nfvres  5149  respreima  5238  isoini  5400  offval  5661  tfrlem5  5871  peano5nni  7698  ixxdisj  8542  icodisj  8630  fzdisj  8686  uzdisj  8725  nn0disj  8765  fzouzdisj  8806  bdinex1  9354  bj-indind  9391  peano5setOLD  9400
 Copyright terms: Public domain W3C validator