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  5959  offval  6243  tfrlem5  6480  mapval2  6847  ixpin  6892  ssenen  7037  infidc  7133  fnfi  7135  peano5nnnn  8112  peano5nni  9146  ixxdisj  10138  icodisj  10227  fzdisj  10287  uzdisj  10328  nn0disj  10373  fzouzdisj  10417  isumss  11957  fsumsplit  11973  sumsplitdc  11998  fsum2dlemstep  12000  fprod2dlemstep  12188  bitsmod  12522  bitsinv1  12528  4sqlem12  12980  nninfdclemcl  13074  nninfdclemp1  13076  insubm  13573  isrhm  14178  subsubrng2  14235  subsubrg2  14266  2idlelb  14525  isbasis2g  14775  tgval2  14781  tgcl  14794  epttop  14820  ssntr  14852  ntreq0  14862  cnptopresti  14968  cnptoprest  14969  cnptoprest2  14970  lmss  14976  txcnp  15001  txcnmpt  15003  bldisj  15131  blininf  15154  blres  15164  metrest  15236  pilem1  15509  wlk1walkdom  16216  trlsegvdegfi  16324  bj-charfundcALT  16430  bj-charfunr  16431  bdinex1  16520  bj-indind  16553