Theorem elin 3342

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	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Proof of Theorem elin

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2771	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2771	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 277	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2256	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2256	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 473	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3159	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2907	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 705	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   _Vcvv 2760   i^i cin 3152

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159

This theorem is referenced by:  elini  3343  elind  3344  elinel1  3345  elinel2  3346  elin2  3347  elin3  3350  incom  3351  ineqri  3352  ineq1  3353  inass  3369  inss1  3379  ssin  3381  ssrin  3384  dfss4st  3392  inssdif  3395  difin  3396  unssin  3398  inssun  3399  invdif  3401  indif  3402  indi  3406  undi  3407  difundi  3411  difindiss  3413  indifdir  3415  difin2  3421  inrab2  3432  inelcm  3507  inssdif0im  3514  uniin  3855  intun  3901  intpr  3902  elrint  3910  iunin2  3976  iinin2m  3981  elriin  3983  disjnim  4020  disjiun  4024  brin  4081  trin  4137  inex1  4163  inuni  4184  bnd2  4202  ordpwsucss  4599  ordpwsucexmid  4602  peano5  4630  inopab  4794  inxp  4796  dmin  4870  opelres  4947  intasym  5050  asymref  5051  dminss  5080  imainss  5081  inimasn  5083  ssrnres  5108  cnvresima  5155  dfco2a  5166  funinsn  5303  imainlem  5335  imain  5336  2elresin  5365  nfvres  5588  respreima  5686  isoini  5861  offval  6138  tfrlem5  6367  mapval2  6732  ixpin  6777  ssenen  6907  infidc  6993  fnfi  6995  peano5nnnn  7952  peano5nni  8985  ixxdisj  9969  icodisj  10058  fzdisj  10118  uzdisj  10159  nn0disj  10204  fzouzdisj  10247  isumss  11534  fsumsplit  11550  sumsplitdc  11575  fsum2dlemstep  11577  fprod2dlemstep  11765  4sqlem12  12540  nninfdclemcl  12605  nninfdclemp1  12607  insubm  13057  isrhm  13654  subsubrng2  13711  subsubrg2  13742  2idlelb  14001  isbasis2g  14213  tgval2  14219  tgcl  14232  epttop  14258  ssntr  14290  ntreq0  14300  cnptopresti  14406  cnptoprest  14407  cnptoprest2  14408  lmss  14414  txcnp  14439  txcnmpt  14441  bldisj  14569  blininf  14592  blres  14602  metrest  14674  pilem1  14914  bj-charfundcALT  15301  bj-charfunr  15302  bdinex1  15391  bj-indind  15424