Theorem elin 3343

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2164  Vcvv 2760   ∩ cin 3153

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160

This theorem is referenced by:  elini  3344  elind  3345  elinel1  3346  elinel2  3347  elin2  3348  elin3  3351  incom  3352  ineqri  3353  ineq1  3354  inass  3370  inss1  3380  ssin  3382  ssrin  3385  dfss4st  3393  inssdif  3396  difin  3397  unssin  3399  inssun  3400  invdif  3402  indif  3403  indi  3407  undi  3408  difundi  3412  difindiss  3414  indifdir  3416  difin2  3422  inrab2  3433  inelcm  3508  inssdif0im  3515  uniin  3856  intun  3902  intpr  3903  elrint  3911  iunin2  3977  iinin2m  3982  elriin  3984  disjnim  4021  disjiun  4025  brin  4082  trin  4138  inex1  4164  inuni  4185  bnd2  4203  ordpwsucss  4600  ordpwsucexmid  4603  peano5  4631  inopab  4795  inxp  4797  dmin  4871  opelres  4948  intasym  5051  asymref  5052  dminss  5081  imainss  5082  inimasn  5084  ssrnres  5109  cnvresima  5156  dfco2a  5167  funinsn  5304  imainlem  5336  imain  5337  2elresin  5366  nfvres  5589  respreima  5687  isoini  5862  offval  6140  tfrlem5  6369  mapval2  6734  ixpin  6779  ssenen  6909  infidc  6995  fnfi  6997  peano5nnnn  7954  peano5nni  8987  ixxdisj  9972  icodisj  10061  fzdisj  10121  uzdisj  10162  nn0disj  10207  fzouzdisj  10250  isumss  11537  fsumsplit  11553  sumsplitdc  11578  fsum2dlemstep  11580  fprod2dlemstep  11768  4sqlem12  12543  nninfdclemcl  12608  nninfdclemp1  12610  insubm  13060  isrhm  13657  subsubrng2  13714  subsubrg2  13745  2idlelb  14004  isbasis2g  14224  tgval2  14230  tgcl  14243  epttop  14269  ssntr  14301  ntreq0  14311  cnptopresti  14417  cnptoprest  14418  cnptoprest2  14419  lmss  14425  txcnp  14450  txcnmpt  14452  bldisj  14580  blininf  14603  blres  14613  metrest  14685  pilem1  14955  bj-charfundcALT  15371  bj-charfunr  15372  bdinex1  15461  bj-indind  15494