Theorem elin 3388

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 2812	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2812	. . 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 3204	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2951	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 709	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

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

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 2802  df-in 3204

This theorem is referenced by:  elini  3389  elind  3390  elinel1  3391  elinel2  3392  elin2  3393  elin3  3396  incom  3397  ineqri  3398  ineq1  3399  inass  3415  inss1  3425  ssin  3427  ssrin  3430  dfss4st  3438  inssdif  3441  difin  3442  unssin  3444  inssun  3445  invdif  3447  indif  3448  indi  3452  undi  3453  difundi  3457  difindiss  3459  indifdir  3461  difin2  3467  inrab2  3478  inelcm  3553  inssdif0im  3560  uniin  3911  intun  3957  intpr  3958  elrint  3966  iunin2  4032  iinin2m  4037  elriin  4039  disjnim  4076  disjiun  4081  brin  4139  trin  4195  inex1  4221  inuni  4243  bnd2  4261  ordpwsucss  4663  ordpwsucexmid  4666  peano5  4694  inopab  4860  inxp  4862  dmin  4937  opelres  5016  intasym  5119  asymref  5120  dminss  5149  imainss  5150  inimasn  5152  ssrnres  5177  cnvresima  5224  dfco2a  5235  funinsn  5376  imainlem  5408  imain  5409  2elresin  5440  nfvres  5671  respreima  5771  isoini  5954  offval  6238  tfrlem5  6475  mapval2  6842  ixpin  6887  ssenen  7032  infidc  7124  fnfi  7126  peano5nnnn  8102  peano5nni  9136  ixxdisj  10128  icodisj  10217  fzdisj  10277  uzdisj  10318  nn0disj  10363  fzouzdisj  10407  isumss  11942  fsumsplit  11958  sumsplitdc  11983  fsum2dlemstep  11985  fprod2dlemstep  12173  bitsmod  12507  bitsinv1  12513  4sqlem12  12965  nninfdclemcl  13059  nninfdclemp1  13061  insubm  13558  isrhm  14162  subsubrng2  14219  subsubrg2  14250  2idlelb  14509  isbasis2g  14759  tgval2  14765  tgcl  14778  epttop  14804  ssntr  14836  ntreq0  14846  cnptopresti  14952  cnptoprest  14953  cnptoprest2  14954  lmss  14960  txcnp  14985  txcnmpt  14987  bldisj  15115  blininf  15138  blres  15148  metrest  15220  pilem1  15493  wlk1walkdom  16156  bj-charfundcALT  16340  bj-charfunr  16341  bdinex1  16430  bj-indind  16463