Theorem elin 3355

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  Vcvv 2771   ∩ cin 3164

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-in 3171

This theorem is referenced by:  elini  3356  elind  3357  elinel1  3358  elinel2  3359  elin2  3360  elin3  3363  incom  3364  ineqri  3365  ineq1  3366  inass  3382  inss1  3392  ssin  3394  ssrin  3397  dfss4st  3405  inssdif  3408  difin  3409  unssin  3411  inssun  3412  invdif  3414  indif  3415  indi  3419  undi  3420  difundi  3424  difindiss  3426  indifdir  3428  difin2  3434  inrab2  3445  inelcm  3520  inssdif0im  3527  uniin  3869  intun  3915  intpr  3916  elrint  3924  iunin2  3990  iinin2m  3995  elriin  3997  disjnim  4034  disjiun  4038  brin  4095  trin  4151  inex1  4177  inuni  4198  bnd2  4216  ordpwsucss  4614  ordpwsucexmid  4617  peano5  4645  inopab  4809  inxp  4811  dmin  4885  opelres  4963  intasym  5066  asymref  5067  dminss  5096  imainss  5097  inimasn  5099  ssrnres  5124  cnvresima  5171  dfco2a  5182  funinsn  5322  imainlem  5354  imain  5355  2elresin  5386  nfvres  5609  respreima  5707  isoini  5886  offval  6165  tfrlem5  6399  mapval2  6764  ixpin  6809  ssenen  6947  infidc  7035  fnfi  7037  peano5nnnn  8004  peano5nni  9038  ixxdisj  10024  icodisj  10113  fzdisj  10173  uzdisj  10214  nn0disj  10259  fzouzdisj  10302  isumss  11673  fsumsplit  11689  sumsplitdc  11714  fsum2dlemstep  11716  fprod2dlemstep  11904  bitsmod  12238  bitsinv1  12244  4sqlem12  12696  nninfdclemcl  12790  nninfdclemp1  12792  insubm  13288  isrhm  13891  subsubrng2  13948  subsubrg2  13979  2idlelb  14238  isbasis2g  14488  tgval2  14494  tgcl  14507  epttop  14533  ssntr  14565  ntreq0  14575  cnptopresti  14681  cnptoprest  14682  cnptoprest2  14683  lmss  14689  txcnp  14714  txcnmpt  14716  bldisj  14844  blininf  14867  blres  14877  metrest  14949  pilem1  15222  bj-charfundcALT  15707  bj-charfunr  15708  bdinex1  15797  bj-indind  15830