Theorem elin 3387

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  Vcvv 2799   ∩ cin 3196

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203

This theorem is referenced by:  elini  3388  elind  3389  elinel1  3390  elinel2  3391  elin2  3392  elin3  3395  incom  3396  ineqri  3397  ineq1  3398  inass  3414  inss1  3424  ssin  3426  ssrin  3429  dfss4st  3437  inssdif  3440  difin  3441  unssin  3443  inssun  3444  invdif  3446  indif  3447  indi  3451  undi  3452  difundi  3456  difindiss  3458  indifdir  3460  difin2  3466  inrab2  3477  inelcm  3552  inssdif0im  3559  uniin  3908  intun  3954  intpr  3955  elrint  3963  iunin2  4029  iinin2m  4034  elriin  4036  disjnim  4073  disjiun  4078  brin  4136  trin  4192  inex1  4218  inuni  4239  bnd2  4257  ordpwsucss  4659  ordpwsucexmid  4662  peano5  4690  inopab  4854  inxp  4856  dmin  4931  opelres  5010  intasym  5113  asymref  5114  dminss  5143  imainss  5144  inimasn  5146  ssrnres  5171  cnvresima  5218  dfco2a  5229  funinsn  5370  imainlem  5402  imain  5403  2elresin  5434  nfvres  5665  respreima  5765  isoini  5948  offval  6232  tfrlem5  6466  mapval2  6833  ixpin  6878  ssenen  7020  infidc  7112  fnfi  7114  peano5nnnn  8090  peano5nni  9124  ixxdisj  10111  icodisj  10200  fzdisj  10260  uzdisj  10301  nn0disj  10346  fzouzdisj  10390  isumss  11917  fsumsplit  11933  sumsplitdc  11958  fsum2dlemstep  11960  fprod2dlemstep  12148  bitsmod  12482  bitsinv1  12488  4sqlem12  12940  nninfdclemcl  13034  nninfdclemp1  13036  insubm  13533  isrhm  14137  subsubrng2  14194  subsubrg2  14225  2idlelb  14484  isbasis2g  14734  tgval2  14740  tgcl  14753  epttop  14779  ssntr  14811  ntreq0  14821  cnptopresti  14927  cnptoprest  14928  cnptoprest2  14929  lmss  14935  txcnp  14960  txcnmpt  14962  bldisj  15090  blininf  15113  blres  15123  metrest  15195  pilem1  15468  wlk1walkdom  16100  bj-charfundcALT  16227  bj-charfunr  16228  bdinex1  16317  bj-indind  16350