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 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∩ cin 3219

This proof depends on 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 proof 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 used 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  3585  inssdif0imOLD  3593  uniin  3955  intun  4001  intpr  4002  elrint  4010  iunin2  4076  iinin2m  4081  elriin  4083  disjnim  4120  disjiun  4125  brin  4184  trin  4241  inex1  4269  inuni  4293  bnd2  4312  ordpwsucss  4716  ordpwsucexmid  4719  peano5  4747  inopab  4914  inxp  4916  dmin  4991  opelres  5070  intasym  5175  asymref  5176  dminss  5205  imainss  5206  inimasn  5208  ssrnres  5233  cnvresima  5280  dfco2a  5291  funinsn  5433  imainlem  5465  imain  5466  2elresin  5497  nfvres  5735  respreima  5839  isoini  6027  offval  6314  tfrlem5  6589  mapval2  6963  ixpin  7009  ssenen  7156  infidc  7252  fnfi  7254  elfpw  7266  peano5nnnn  8265  peano5nni  9316  ixxdisj  10322  icodisj  10411  fzdisj  10474  uzdisj  10517  nn0disj  10562  fzouzdisj  10606  sseqn  11301  hashfibclem  11304  isumss  12183  fsumsplit  12199  sumsplitdc  12224  fsum2dlemstep  12226  fprod2dlemstep  12414  bitsmod  12748  bitsinv1  12754  4sqlem12  13210  ballotfilem2  13286  ballotfilemth  13339  nninfdclemcl  13397  nninfdclemp1  13399  insubm  13851  resscntz  14166  gsummptfidmsplit  14254  isrhm  14574  subsubrng2  14632  subsubrg2  14663  2idlelb  14951  isassa  15111  aspid  15126  isbasis2g  15271  tgval2  15277  tgcl  15290  epttop  15316  ssntr  15348  ntreq0  15358  cnptopresti  15464  cnptoprest  15465  cnptoprest2  15466  lmss  15472  txcnp  15497  txcnmpt  15499  bldisj  15627  blininf  15650  blres  15660  metrest  15732  pilem1  16006  ppiqsval2  16241  ppiqfi  16242  ppiprm  16259  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  prmorcht  16282  ppiqub  16293  wlk1walkdom  16805  trlsegvdegfi  16913  bj-charfundcALT  17040  bj-charfunr  17041  bdinex1  17130  bj-indind  17163