Theorem incom 3805

Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
incom	⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Proof of Theorem incom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ancom 466	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
2		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
4	1, 2, 3	3bitr4i 292	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
5	4	eqriv 2619	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  ineq2  3808  sseqin2  3817  dfss1OLD  3818  in12  3824  in32  3825  in13  3826  in31  3827  inss2  3834  sslin  3839  inss  3842  indif1  3871  indifcom  3872  indir  3875  dfsymdif3  3893  dfrab2  3903  0in  3969  disjr  4018  ssdifin0  4050  difdifdir  4056  uneqdifeq  4057  uneqdifeqOLD  4058  disjtp2  4252  diftpsn3OLD  4333  iinrab2  4583  iunin1  4585  iinin1  4591  riinn0  4595  disjprg  4648  disjxun  4651  inex2  4800  resiun1OLD  5417  dmres  5419  rescom  5423  resima2OLD  5433  resindm  5444  resdmdfsn  5445  resopab  5446  imadisj  5484  intirr  5514  djudisj  5561  imainrect  5575  dmresv  5593  resdmres  5625  coeq0  5644  dfpred3  5690  wfi  5713  ordtri3or  5755  fnresdisj  6001  fnimaeq0  6013  resasplit  6074  fresaun  6075  fresaunres2  6076  fresaunres1  6077  f0rn0  6090  fvun2  6270  fveqressseq  6355  ressnop0  6420  fninfp  6440  fvsnun1  6448  fsnunfv  6453  fveqf1o  6557  orduniss2  7033  offres  7163  curry1  7269  curry2  7272  fpar  7281  wfrlem5  7419  smores3  7450  oacomf1o  7645  ralxpmap  7907  difsnen  8042  domunsncan  8060  domunsn  8110  limensuci  8136  phplem2  8140  pssnn  8178  dif1en  8193  domunfican  8233  marypha1lem  8339  zfregfr  8509  epfrs  8607  zfregs2  8609  tskwe  8776  dif1card  8833  dfac8b  8854  ac10ct  8857  kmlem11  8982  kmlem12  8983  cdacomen  9003  onacda  9019  ackbij1lem14  9055  ackbij1lem16  9057  ackbij1lem18  9059  fin23lem26  9147  fin23lem19  9158  fin23lem30  9164  isf32lem4  9178  isf34lem7  9201  isf34lem6  9202  axdc3lem4  9275  brdom7disj  9353  brdom6disj  9354  fpwwe2lem13  9464  canthp1lem1  9474  grothprim  9656  fzpreddisj  12390  fzdifsuc  12400  fseq1p1m1  12414  prinfzo0  12506  hashgval  13120  hashun3  13173  hashfun  13224  hashbclem  13236  xpcoidgend  13714  cotr2  13716  limsupgle  14208  prmreclem2  15621  setsdm  15892  setsfun  15893  setsfun0  15894  setsid  15914  ressinbas  15936  wunress  15940  mreexexlem2d  16305  mreexexlem4d  16307  oppcinv  16440  cnvps  17212  pmtrmvd  17876  lsmmod2  18089  lsmdisj3  18096  lsmdisjr  18097  lsmdisj2r  18098  lsmdisj3r  18099  lsmdisj2a  18100  lsmdisj2b  18101  lsmdisj3a  18102  lsmdisj3b  18103  subgdisj2  18105  pj2f  18111  pj1id  18112  frgpuplem  18185  gsummptfzsplitl  18333  dprd2da  18441  dmdprdsplit2lem  18444  dmdprdsplit2  18445  pgpfaclem1  18480  lmhmlsp  19049  pwssplit1  19059  ltbwe  19472  psrbag0  19494  cnfldfun  19758  psgndiflemB  19946  pjpm  20052  islindf4  20177  elcls  20877  mretopd  20896  restin  20970  restcld  20976  neitr  20984  resstopn  20990  lecldbas  21023  nrmsep  21161  regsep2  21180  isreg2  21181  ordthaus  21188  cmpsublem  21202  cmpsub  21203  hauscmplem  21209  bwth  21213  iunconn  21231  cldllycmp  21298  kgentopon  21341  llycmpkgen2  21353  1stckgen  21357  txkgen  21455  kqcldsat  21536  regr1lem2  21543  fbun  21644  fin1aufil  21736  fclsfnflim  21831  ustexsym  22019  restutopopn  22042  ustuqtop5  22049  ressuss  22067  metreslem  22167  blcld  22310  ressxms  22330  ressms  22331  restmetu  22375  reconn  22631  metdseq0  22657  metnrmlem3  22664  unmbl  23305  volun  23313  volinun  23314  iundisj2  23317  icombl  23332  ioombl  23333  uniioombllem2  23351  uniioombllem4  23354  dyaddisjlem  23363  dyaddisj  23364  mbfconstlem  23396  mbfeqalem  23409  ismbf3d  23421  itg1addlem5  23467  itgsplitioo  23604  lhop  23779  tdeglem4  23820  vieta1lem2  24066  xrlimcnp  24695  perfectlem2  24955  rplogsum  25216  perpcom  25608  vtxdgoddnumeven  26449  ex-dif  27280  ococi  28264  orthin  28305  lediri  28396  pjoml2i  28444  pjoml4i  28446  cmcmlem  28450  cmbr3i  28459  cmm2i  28466  cm0  28468  fh1  28477  fh2  28478  cm2j  28479  qlaxr3i  28495  pjclem2  29055  stm1ri  29103  golem1  29130  dmdbr5  29167  mddmd2  29168  cvmdi  29183  mdsldmd1i  29190  csmdsymi  29193  mdexchi  29194  cvexchi  29228  atssma  29237  atomli  29241  atoml2i  29242  atordi  29243  atcvatlem  29244  chirredlem1  29249  chirredlem2  29250  chirredlem3  29251  atcvat4i  29256  atabsi  29260  mdsymlem1  29262  dmdbr6ati  29282  cdj3lem3  29297  inin  29352  difeq  29355  difuncomp  29369  disjdifprg  29388  iundisj2f  29403  disjunsn  29407  imadifxp  29414  fnresin  29430  df1stres  29481  df2ndres  29482  padct  29497  iocinif  29543  difioo  29544  iundisj2fi  29556  xrge00  29686  xrge0slmod  29844  lmxrge0  29998  esumrnmpt2  30130  esumpfinvallem  30136  ldgenpisyslem1  30226  ldgenpisys  30229  measxun2  30273  measunl  30279  carsgclctunlem1  30379  carsgclctunlem2  30381  eulerpartlemt  30433  eulerpartgbij  30434  probmeasb  30492  bayesth  30501  ballotlemfp1  30553  ballotlemfval0  30557  signstres  30652  hashreprin  30698  reprfz1  30702  chtvalz  30707  breprexpnat  30712  subfacp1lem3  31164  subfacp1lem5  31166  pconnconn  31213  cvmscld  31255  cvmsss2  31256  mrsubvrs  31419  mthmpps  31479  frind  31740  frrlem5  31784  nosupbnd2lem1  31861  noetalem2  31864  noetalem3  31865  cldbnd  32321  bj-inrab3  32925  bj-2upln1upl  33012  bj-sscon  33014  bj-rest0  33046  bj-0int  33055  bj-diagval  33090  icoreclin  33205  fin2so  33396  ptrest  33408  poimirlem3  33412  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem18  33427  poimirlem19  33428  poimirlem21  33430  poimirlem22  33431  poimirlem27  33436  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  cnambfre  33458  asindmre  33495  dvasin  33496  dvreasin  33498  dvreacos  33499  sstotbnd2  33573  bndss  33585  ineqcom  34005  inres2  34007  inex2ALTV  34105  l1cvat  34342  pmod2iN  35135  pmodN  35136  pmodl42N  35137  osumcllem3N  35244  osumcllem4N  35245  dihmeetlem19N  36614  dihmeetALTN  36616  elrfi  37257  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  diophin  37336  diophren  37377  dnwech  37618  fnwe2lem2  37621  kelac1  37633  kelac2lem  37634  kelac2  37635  lmhmlnmsplit  37657  pwssplit4  37659  pwfi2f1o  37666  proot1hash  37778  rp-fakeuninass  37862  elcnvcnvintab  37888  relintab  37889  elcnvcnvlem  37905  conrel1d  37955  dfrcl2  37966  iunrelexp0  37994  ntrk0kbimka  38337  neicvgbex  38410  hashnzfz  38519  zfregs2VD  39076  iunconnlem2  39171  ssinss2d  39228  restuni4  39304  restuni6  39305  iccdifioo  39741  uzinico2  39789  sumnnodd  39862  limsupvaluz  39940  cncfuni  40099  fouriersw  40448  saliincl  40545  iundjiunlem  40676  iundjiun  40677  caragenuncllem  40726  caragendifcl  40728  isomenndlem  40744  hoidmvlelem2  40810  smflimlem1  40979  perfectALTVlem2  41631  rnghmsscmap2  41973  rnghmsubcsetclem1  41975  rnghmsubcsetc  41977  rngccat  41978  rngcid  41979  rngchomrnghmresALTV  41996  rngcifuestrc  41997  funcrngcsetc  41998  rhmsscmap2  42019  rhmsubcsetclem1  42021  rhmsubcsetc  42023  ringccat  42024  ringcid  42025  rhmsscrnghm  42026  rhmsubcrngclem1  42027  rhmsubcrngc  42029  rngcresringcat  42030  funcringcsetc  42035  rngcrescrhm  42085  rhmsubclem3  42088  rhmsubc  42090  rngcrescrhmALTV  42103  rhmsubcALTVlem3  42106  rhmsubcALTVlem4  42107