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

Theorem elin 3262
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 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem elin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elex 2700 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2700 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 275 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2203 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2203 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 465 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3080 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 2834 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 694 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104   = wceq 1332  wcel 1481  Vcvv 2689  cin 3073
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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3080
This theorem is referenced by:  elini  3263  elind  3264  elinel1  3265  elinel2  3266  elin2  3267  elin3  3270  incom  3271  ineqri  3272  ineq1  3273  inass  3289  inss1  3299  ssin  3301  ssrin  3304  dfss4st  3312  inssdif  3315  difin  3316  unssin  3318  inssun  3319  invdif  3321  indif  3322  indi  3326  undi  3327  difundi  3331  difindiss  3333  indifdir  3335  difin2  3341  inrab2  3352  inelcm  3426  inssdif0im  3433  uniin  3762  intun  3808  intpr  3809  elrint  3817  iunin2  3882  iinin2m  3887  elriin  3889  disjnim  3926  disjiun  3930  brin  3986  trin  4042  inex1  4068  inuni  4086  bnd2  4103  ordpwsucss  4488  ordpwsucexmid  4491  peano5  4518  inopab  4677  inxp  4679  dmin  4753  opelres  4830  intasym  4929  asymref  4930  dminss  4959  imainss  4960  inimasn  4962  ssrnres  4987  cnvresima  5034  dfco2a  5045  funinsn  5178  imainlem  5210  imain  5211  2elresin  5240  nfvres  5460  respreima  5554  isoini  5725  offval  5995  tfrlem5  6217  mapval2  6578  ixpin  6623  ssenen  6751  fnfi  6831  peano5nnnn  7722  peano5nni  8745  ixxdisj  9714  icodisj  9803  fzdisj  9861  uzdisj  9902  nn0disj  9944  fzouzdisj  9986  isumss  11190  fsumsplit  11206  sumsplitdc  11231  fsum2dlemstep  11233  isbasis2g  12244  tgval2  12252  tgcl  12265  epttop  12291  ssntr  12323  ntreq0  12333  cnptopresti  12439  cnptoprest  12440  cnptoprest2  12441  lmss  12447  txcnp  12472  txcnmpt  12474  bldisj  12602  blininf  12625  blres  12635  metrest  12707  pilem1  12901  bdinex1  13261  bj-indind  13294
  Copyright terms: Public domain W3C validator