Theorem elin 3412

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 2833	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2833	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 277	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 477	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3226	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2973	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 716	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∩ cin 3219

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226

This theorem is referenced by:  elini  3413  elind  3414  elinel1  3415  elinel2  3416  elin2  3417  elin3  3420  incom  3421  ineqri  3424  ineq1  3425  inass  3441  inss1  3451  ssin  3453  ssrin  3456  dfss4st  3464  inssdif  3467  difin  3468  unssin  3470  inssun  3471  invdif  3473  indif  3474  indi  3478  undi  3479  difundi  3483  difindiss  3485  indifdir  3487  difin2  3493  inrab2  3506  inelcm  3584  inssdif0im  3591  uniin  3950  intun  3996  intpr  3997  elrint  4005  iunin2  4071  iinin2m  4076  elriin  4078  disjnim  4115  disjiun  4120  brin  4178  trin  4234  inex1  4262  inuni  4286  bnd2  4305  ordpwsucss  4709  ordpwsucexmid  4712  peano5  4740  inopab  4907  inxp  4909  dmin  4984  opelres  5063  intasym  5167  asymref  5168  dminss  5197  imainss  5198  inimasn  5200  ssrnres  5225  cnvresima  5272  dfco2a  5283  funinsn  5425  imainlem  5457  imain  5458  2elresin  5489  nfvres  5726  respreima  5827  isoini  6014  offval  6300  tfrlem5  6575  mapval2  6949  ixpin  6995  ssenen  7142  infidc  7238  fnfi  7240  elfpw  7252  peano5nnnn  8249  peano5nni  9286  ixxdisj  10284  icodisj  10373  fzdisj  10435  uzdisj  10478  nn0disj  10523  fzouzdisj  10567  sseqn  11257  hashfibclem  11260  isumss  12136  fsumsplit  12152  sumsplitdc  12177  fsum2dlemstep  12179  fprod2dlemstep  12367  bitsmod  12701  bitsinv1  12707  4sqlem12  13159  ballotfilem2  13206  ballotfilemth  13259  nninfdclemcl  13317  nninfdclemp1  13319  insubm  13769  isrhm  14438  subsubrng2  14496  subsubrg2  14527  2idlelb  14814  isbasis2g  15069  tgval2  15075  tgcl  15088  epttop  15114  ssntr  15146  ntreq0  15156  cnptopresti  15262  cnptoprest  15263  cnptoprest2  15264  lmss  15270  txcnp  15295  txcnmpt  15297  bldisj  15425  blininf  15448  blres  15458  metrest  15530  pilem1  15803  wlk1walkdom  16514  trlsegvdegfi  16622  bj-charfundcALT  16749  bj-charfunr  16750  bdinex1  16839  bj-indind  16872