Theorem elin 3412

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 2833	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2833	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 277	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2301	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 477	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3226	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2973	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 716	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ∩ cin 3219

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226

This theorem is used by:  elini  3413  elind  3414  elinel1  3415  elinel2  3416  elin2  3417  elin3  3420  incom  3421  ineqri  3424  ineq1  3425  inass  3441  inss1  3451  ssin  3453  ssrin  3456  dfss4st  3464  inssdif  3467  difin  3468  unssin  3470  inssun  3471  invdif  3473  indif  3474  indi  3478  undi  3479  difundi  3483  difindiss  3485  indifdir  3487  difin2  3493  inrab2  3506  inelcm  3585  inssdif0imOLD  3593  uniin  3955  intun  4001  intpr  4002  elrint  4010  iunin2  4076  iinin2m  4081  elriin  4083  disjnim  4120  disjiun  4125  brin  4184  trin  4241  inex1  4269  inuni  4293  bnd2  4312  ordpwsucss  4716  ordpwsucexmid  4719  peano5  4747  inopab  4914  inxp  4916  dmin  4991  opelres  5070  intasym  5175  asymref  5176  dminss  5205  imainss  5206  inimasn  5208  ssrnres  5233  cnvresima  5280  dfco2a  5291  funinsn  5433  imainlem  5465  imain  5466  2elresin  5497  nfvres  5735  respreima  5839  isoini  6027  offval  6314  tfrlem5  6590  mapval2  6964  ixpin  7011  ssenen  7158  infidc  7254  fnfi  7256  elfpw  7268  peano5nnnn  8265  peano5nni  9316  ixxdisj  10321  icodisj  10410  fzdisj  10473  uzdisj  10516  nn0disj  10561  fzouzdisj  10605  sseqn  11300  hashfibclem  11303  isumss  12182  fsumsplit  12198  sumsplitdc  12223  fsum2dlemstep  12225  fprod2dlemstep  12413  bitsmod  12747  bitsinv1  12753  4sqlem12  13209  ballotfilem2  13285  ballotfilemth  13338  nninfdclemcl  13396  nninfdclemp1  13398  insubm  13850  resscntz  14165  gsummptfidmsplit  14253  isrhm  14573  subsubrng2  14631  subsubrg2  14662  2idlelb  14950  isassa  15110  aspid  15125  isbasis2g  15288  tgval2  15294  tgcl  15307  epttop  15333  ssntr  15365  ntreq0  15375  cnptopresti  15481  cnptoprest  15482  cnptoprest2  15483  lmss  15489  txcnp  15514  txcnmpt  15516  bldisj  15644  blininf  15667  blres  15677  metrest  15749  pilem1  16023  ppiqsval2  16258  ppiqfi  16259  ppiprm  16276  chtprm  16278  chtdif  16281  efchtqdvds  16282  ppidif  16286  prmorcht  16299  ppiqub  16310  wlk1walkdom  16822  trlsegvdegfi  16930  bj-charfundcALT  17057  bj-charfunr  17058  bdinex1  17147  bj-indind  17180