Theorem elin 3356

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2176  Vcvv 2772   ∩ cin 3165

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172

This theorem is referenced by:  elini  3357  elind  3358  elinel1  3359  elinel2  3360  elin2  3361  elin3  3364  incom  3365  ineqri  3366  ineq1  3367  inass  3383  inss1  3393  ssin  3395  ssrin  3398  dfss4st  3406  inssdif  3409  difin  3410  unssin  3412  inssun  3413  invdif  3415  indif  3416  indi  3420  undi  3421  difundi  3425  difindiss  3427  indifdir  3429  difin2  3435  inrab2  3446  inelcm  3521  inssdif0im  3528  uniin  3870  intun  3916  intpr  3917  elrint  3925  iunin2  3991  iinin2m  3996  elriin  3998  disjnim  4035  disjiun  4039  brin  4096  trin  4152  inex1  4178  inuni  4199  bnd2  4217  ordpwsucss  4615  ordpwsucexmid  4618  peano5  4646  inopab  4810  inxp  4812  dmin  4886  opelres  4964  intasym  5067  asymref  5068  dminss  5097  imainss  5098  inimasn  5100  ssrnres  5125  cnvresima  5172  dfco2a  5183  funinsn  5323  imainlem  5355  imain  5356  2elresin  5387  nfvres  5610  respreima  5708  isoini  5887  offval  6166  tfrlem5  6400  mapval2  6765  ixpin  6810  ssenen  6948  infidc  7036  fnfi  7038  peano5nnnn  8005  peano5nni  9039  ixxdisj  10025  icodisj  10114  fzdisj  10174  uzdisj  10215  nn0disj  10260  fzouzdisj  10304  isumss  11702  fsumsplit  11718  sumsplitdc  11743  fsum2dlemstep  11745  fprod2dlemstep  11933  bitsmod  12267  bitsinv1  12273  4sqlem12  12725  nninfdclemcl  12819  nninfdclemp1  12821  insubm  13317  isrhm  13920  subsubrng2  13977  subsubrg2  14008  2idlelb  14267  isbasis2g  14517  tgval2  14523  tgcl  14536  epttop  14562  ssntr  14594  ntreq0  14604  cnptopresti  14710  cnptoprest  14711  cnptoprest2  14712  lmss  14718  txcnp  14743  txcnmpt  14745  bldisj  14873  blininf  14896  blres  14906  metrest  14978  pilem1  15251  bj-charfundcALT  15745  bj-charfunr  15746  bdinex1  15835  bj-indind  15868