Theorem elin 3390

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 2814	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2814	. . 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 3206	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2953	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 711	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  Vcvv 2802   ∩ cin 3199

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206

This theorem is referenced by:  elini  3391  elind  3392  elinel1  3393  elinel2  3394  elin2  3395  elin3  3398  incom  3399  ineqri  3400  ineq1  3401  inass  3417  inss1  3427  ssin  3429  ssrin  3432  dfss4st  3440  inssdif  3443  difin  3444  unssin  3446  inssun  3447  invdif  3449  indif  3450  indi  3454  undi  3455  difundi  3459  difindiss  3461  indifdir  3463  difin2  3469  inrab2  3480  inelcm  3555  inssdif0im  3562  uniin  3913  intun  3959  intpr  3960  elrint  3968  iunin2  4034  iinin2m  4039  elriin  4041  disjnim  4078  disjiun  4083  brin  4141  trin  4197  inex1  4223  inuni  4245  bnd2  4263  ordpwsucss  4665  ordpwsucexmid  4668  peano5  4696  inopab  4862  inxp  4864  dmin  4939  opelres  5018  intasym  5121  asymref  5122  dminss  5151  imainss  5152  inimasn  5154  ssrnres  5179  cnvresima  5226  dfco2a  5237  funinsn  5379  imainlem  5411  imain  5412  2elresin  5443  nfvres  5675  respreima  5775  isoini  5958  offval  6242  tfrlem5  6479  mapval2  6846  ixpin  6891  ssenen  7036  infidc  7132  fnfi  7134  peano5nnnn  8111  peano5nni  9145  ixxdisj  10137  icodisj  10226  fzdisj  10286  uzdisj  10327  nn0disj  10372  fzouzdisj  10416  isumss  11951  fsumsplit  11967  sumsplitdc  11992  fsum2dlemstep  11994  fprod2dlemstep  12182  bitsmod  12516  bitsinv1  12522  4sqlem12  12974  nninfdclemcl  13068  nninfdclemp1  13070  insubm  13567  isrhm  14171  subsubrng2  14228  subsubrg2  14259  2idlelb  14518  isbasis2g  14768  tgval2  14774  tgcl  14787  epttop  14813  ssntr  14845  ntreq0  14855  cnptopresti  14961  cnptoprest  14962  cnptoprest2  14963  lmss  14969  txcnp  14994  txcnmpt  14996  bldisj  15124  blininf  15147  blres  15157  metrest  15229  pilem1  15502  wlk1walkdom  16209  bj-charfundcALT  16404  bj-charfunr  16405  bdinex1  16494  bj-indind  16527