Theorem elin 3316

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 2746	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2746	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 277	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2238	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2238	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 473	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3133	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2882	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 704	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2146  Vcvv 2735   ∩ cin 3126

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-in 3133

This theorem is referenced by:  elini  3317  elind  3318  elinel1  3319  elinel2  3320  elin2  3321  elin3  3324  incom  3325  ineqri  3326  ineq1  3327  inass  3343  inss1  3353  ssin  3355  ssrin  3358  dfss4st  3366  inssdif  3369  difin  3370  unssin  3372  inssun  3373  invdif  3375  indif  3376  indi  3380  undi  3381  difundi  3385  difindiss  3387  indifdir  3389  difin2  3395  inrab2  3406  inelcm  3481  inssdif0im  3488  uniin  3825  intun  3871  intpr  3872  elrint  3880  iunin2  3945  iinin2m  3950  elriin  3952  disjnim  3989  disjiun  3993  brin  4050  trin  4106  inex1  4132  inuni  4150  bnd2  4168  ordpwsucss  4560  ordpwsucexmid  4563  peano5  4591  inopab  4752  inxp  4754  dmin  4828  opelres  4905  intasym  5005  asymref  5006  dminss  5035  imainss  5036  inimasn  5038  ssrnres  5063  cnvresima  5110  dfco2a  5121  funinsn  5257  imainlem  5289  imain  5290  2elresin  5319  nfvres  5540  respreima  5636  isoini  5809  offval  6080  tfrlem5  6305  mapval2  6668  ixpin  6713  ssenen  6841  fnfi  6926  peano5nnnn  7866  peano5nni  8893  ixxdisj  9872  icodisj  9961  fzdisj  10020  uzdisj  10061  nn0disj  10106  fzouzdisj  10148  isumss  11365  fsumsplit  11381  sumsplitdc  11406  fsum2dlemstep  11408  fprod2dlemstep  11596  nninfdclemcl  12414  nninfdclemp1  12416  insubm  12732  isbasis2g  13094  tgval2  13102  tgcl  13115  epttop  13141  ssntr  13173  ntreq0  13183  cnptopresti  13289  cnptoprest  13290  cnptoprest2  13291  lmss  13297  txcnp  13322  txcnmpt  13324  bldisj  13452  blininf  13475  blres  13485  metrest  13557  pilem1  13751  bj-charfundcALT  14101  bj-charfunr  14102  bdinex1  14191  bj-indind  14224