Theorem elin 3392

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.

Step	Hyp	Ref	Expression
1		elex 2815	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2815	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 277	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2294	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2294	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 473	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3207	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2954	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 712	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2202  Vcvv 2803   ∩ cin 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207

This theorem is referenced by:  elini  3393  elind  3394  elinel1  3395  elinel2  3396  elin2  3397  elin3  3400  incom  3401  ineqri  3402  ineq1  3403  inass  3419  inss1  3429  ssin  3431  ssrin  3434  dfss4st  3442  inssdif  3445  difin  3446  unssin  3448  inssun  3449  invdif  3451  indif  3452  indi  3456  undi  3457  difundi  3461  difindiss  3463  indifdir  3465  difin2  3471  inrab2  3482  inelcm  3557  inssdif0im  3564  uniin  3918  intun  3964  intpr  3965  elrint  3973  iunin2  4039  iinin2m  4044  elriin  4046  disjnim  4083  disjiun  4088  brin  4146  trin  4202  inex1  4228  inuni  4250  bnd2  4269  ordpwsucss  4671  ordpwsucexmid  4674  peano5  4702  inopab  4868  inxp  4870  dmin  4945  opelres  5024  intasym  5128  asymref  5129  dminss  5158  imainss  5159  inimasn  5161  ssrnres  5186  cnvresima  5233  dfco2a  5244  funinsn  5386  imainlem  5418  imain  5419  2elresin  5450  nfvres  5684  respreima  5783  isoini  5969  offval  6252  tfrlem5  6523  mapval2  6890  ixpin  6935  ssenen  7080  infidc  7176  fnfi  7178  peano5nnnn  8155  peano5nni  9188  ixxdisj  10182  icodisj  10271  fzdisj  10332  uzdisj  10373  nn0disj  10418  fzouzdisj  10462  isumss  12015  fsumsplit  12031  sumsplitdc  12056  fsum2dlemstep  12058  fprod2dlemstep  12246  bitsmod  12580  bitsinv1  12586  4sqlem12  13038  nninfdclemcl  13132  nninfdclemp1  13134  insubm  13631  isrhm  14236  subsubrng2  14293  subsubrg2  14324  2idlelb  14584  isbasis2g  14839  tgval2  14845  tgcl  14858  epttop  14884  ssntr  14916  ntreq0  14926  cnptopresti  15032  cnptoprest  15033  cnptoprest2  15034  lmss  15040  txcnp  15065  txcnmpt  15067  bldisj  15195  blininf  15218  blres  15228  metrest  15300  pilem1  15573  wlk1walkdom  16283  trlsegvdegfi  16391  bj-charfundcALT  16508  bj-charfunr  16509  bdinex1  16598  bj-indind  16631