Theorem elin 2251

Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25.

Assertion

Ref	Expression
elin	|- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Proof of Theorem elin

Step	Hyp	Ref	Expression
1		elisset 1855	. 2 |- (A e. (B i^i C) -> A e. V)
2		elisset 1855	. . 3 |- (A e. C -> A e. V)
3	2	adantl 388	. 2 |- ((A e. B /\ A e. C) -> A e. V)
4		eleq1 1571	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1571	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 630	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 2095	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 1938	. 2 |- (A e. V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 682	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 144   /\ wa 221   = wceq 988   e. wcel 990  Vcvv 1849   i^i cin 2090

This theorem is referenced by:  incom 2252  ineqri 2253  ineq1 2254  hbin 2264  rabbirdv 2265  inass 2267  inss1 2274  ssrin 2278  dfss4 2286  dfin2 2288  difin 2289  indi 2295  undi 2296  unineq 2299  inab 2312  inrab2 2316  inelcm 2368  difin0ss 2377  inssdif0 2378  disjsn 2486  uniin 2568  intun 2610  intpr 2611  iunin2 2658  trin 2741  inex1 2767  frirr 2979  wefrc 2998  ordtri3or 3034  ordpwsuc 3121  brinxp2 3290  inopab 3334  inxp 3335  dmin 3382  opelres 3432  dfima2 3468  intasym 3501  asymref 3502  intirr 3504  cnvin 3512  dminss 3518  imainss 3519  ssrnres 3537  dfco3OLD 3569  dfco2a 3570  dfco4OLD 3571  funin 3641  2elresin 3673  nfvres 3824  funfvima 3928  isomin 3975  isoini 3976  tfrlem5 3991  tz7.48-2 4033  mapval2 4422  pw2en 4533  sbthcl 4546  ssenen 4593  inf3lem2 4700  zfregs 4733  cp 4808  bnd2 4810  aceq5lem1 4821  aceq5lem5 4825  aceq5 4826  kmlem3 4853  kmlem14 4864  kmlem15 4865  ltpiord 5104  ltxr 5584  clm4i 7203  infpss 7699  isbasis2g 7736  tgval2 7741  tgcl 7748  tgss3 7762  basgen 7764  opnin 7989  lmss 8073  isphg 8595  ishl 8710  axgroth4 8899  grothprim 8902  axhcompl 8987  hhcmpl 9189  ocin 9289  ocnel 9290  chocunii 9292  projlemHIL 9338  omlsilem 9364  pjoc1i 9384  shmodsi 9482  spansnm0i 9715  nonbooli 9716  5oalem1 9719  5oalem2 9720  5oalem4 9722  5oalem5 9723  5oalem7 9725  3oalem2 9728  3oalem3 9729  pjssmii 9746  mayete3i 9793  nmcopex 10076  nmcoplb 10077  lncnopbd 10083  nmcfnex 10105  nmcfnlb 10106  riesz4 10114  riesz1 10115  riesz2 10116  cnlnadjlem3 10119  cnlnadjlem4 10120  cnlnadjlem5 10121  cnlnadjlem9 10125  cnlnadjeu 10128  rnbra 10157  pjimai 10221  dfpjop 10228  pjclem4a 10244  pjclem4 10245  pj3lem1 10252  pj3si 10253  jpi 10315  sumdmdii 10460  sumdmdlem 10463  sumdmdlem2 10464  cdjreui 10477  cdj3lem1 10479  ntunte 10561  uninqs 10563  uninqsOLD 10564  domintref 10600  int2rel 10601  inposet 10619  filintf 10707  sfvlim 10729  fintopcomp 10747  topunfincomp 10748  usinuniop 10753

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-sb 1205  df-clab 1500  df-cleq 1505  df-clel 1508  df-v 1850  df-in 2095

Copyright terms: Public domain