Theorem incom 4155

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

Assertion

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

Proof of Theorem incom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabswap 3421	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
2		dfin5 3907	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
3		dfin5 3907	. 2 ⊢ (𝐵 ∩ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
4	1, 2, 3	3eqtr4i 2793	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3412   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rab 3413  df-in 3906

This theorem is used by:  ineqcom  4156  ineqcomi  4157  ineq2  4160  in12  4174  in32  4175  in13  4176  in31  4177  inss2  4183  sslin  4188  inss  4194  indif1  4228  indifcom  4229  indir  4232  indifdir  4241  dfsymdif3  4252  dfrab2  4266  difdifdir  4447  disjtp2  4677  iunin1  5030  iinin1  5039  riinn0  5043  disjprg  5099  disjxun  5101  inex2  5281  inex2g  5283  rescom  5995  resindmOLD  6024  resdmdfsnOLD  6026  resopab  6030  imadisj  6076  intirr  6112  djudisj  6159  imainrect  6174  dmresv  6194  resdmres  6228  coeq0  6252  dfpred3  6310  predres  6337  frpoind  6340  ordtri3or  6390  fnresdisj  6653  fnimaeq0  6666  resasplit  6746  fresaun  6747  fresaunres2  6748  fresaunres1  6749  f0rn0  6761  fvun2  6971  rescnvimafod  7067  fveqressseq  7073  ressnop0  7151  fninfp  7173  fsnunfv  7186  f1resrcmplf1d  7273  orduniss2  7830  offres  7981  curry1  8102  curry2  8105  fpar  8114  fprlem1  8300  smores3  8343  oacomf1o  8555  domunsncan  9078  dif1ennnALT  9250  domunfican  9294  marypha1lem  9406  zfregfr  9586  epfrs  9713  zfregs2  9715  frind  9735  frrlem15  9742  djuin  9926  tskwe  9958  kmlem11  10166  kmlem12  10167  djucomen  10183  onadju  10199  ackbij1lem14  10237  ackbij1lem16  10239  fin23lem26  10330  fin23lem19  10341  fin23lem30  10347  isf32lem4  10361  isf34lem7  10384  isf34lem6  10385  axdc3lem4  10458  brdom7disj  10537  brdom6disj  10538  fpwwe2lem12  10654  fzpreddisj  13631  fzdifsuc  13642  fseq1p1m1  13656  prinfzo0  13757  f1resfz0f1d  13851  hashun3  14451  hashbclem  14520  hash7g  14554  xpcoidgend  15051  cotr2  15053  limsupgle  15567  prmreclem2  17012  setsdm  17265  ressinbas  17340  wunress  17344  mreexexlem2d  17736  oppcinv  17872  cnvps  18669  pmtrmvd  19586  lsmmod2  19806  lsmdisj3  19813  lsmdisjr  19814  lsmdisj2r  19815  lsmdisj3r  19816  lsmdisj2a  19817  lsmdisj2b  19818  lsmdisj3a  19819  lsmdisj3b  19820  subgdisj2  19822  pj2f  19828  pj1id  19829  frgpuplem  19902  gsummptfzsplitl  20063  dprd2da  20174  dmdprdsplit2lem  20177  dmdprdsplit2  20178  pgpfaclem1  20213  rnghmsscmap2  20794  rnghmsubcsetclem1  20796  rnghmsubcsetc  20798  rngccat  20799  rngcid  20800  rngcifuestrc  20804  funcrngcsetc  20805  rhmsscmap2  20823  rhmsubcsetclem1  20825  rhmsubcsetc  20827  ringccat  20828  ringcid  20829  rhmsscrnghm  20830  rhmsubcrngclem1  20831  rhmsubcrngc  20833  rngcresringcat  20834  funcringcsetc  20839  rngcrescrhm  20849  rhmsubclem3  20852  rhmsubc  20854  lmhmlsp  21236  ssdifidlprm  21552  psgndiflemB  21816  pjpm  21924  ltbwe  22263  psrbag0  22281  elcls  23301  mretopd  23320  restin  23394  restcld  23400  resstopn  23414  lecldbas  23447  nrmsep  23585  isreg2  23605  ordthaus  23612  cmpsublem  23627  cmpsub  23628  hauscmplem  23634  bwth  23638  iunconn  23656  cldllycmp  23724  kgentopon  23767  llycmpkgen2  23779  1stckgen  23783  txkgen  23881  kqcldsat  23962  regr1lem2  23969  fbun  24069  fin1aufil  24161  fclsfnflim  24256  ustexsym  24445  restutopopn  24467  ustuqtop5  24474  ressuss  24491  metreslem  24591  blcld  24734  ressxms  24754  ressms  24755  reconn  25058  metdseq0  25084  metnrmlem3  25091  unmbl  25768  volun  25776  iundisj2  25780  icombl  25795  ioombl  25796  uniioombllem2  25814  uniioombllem4  25817  dyaddisjlem  25826  dyaddisj  25827  mbfconstlem  25858  mbfeqalem2  25873  ismbf3d  25885  itg1addlem5  25931  itgsplitioo  26068  lhop  26246  vieta1lem2  26546  perfectlem2  27469  rplogsum  27766  nosupbnd2lem1  27954  ltslpss  28176  leslss  28177  perpcom  29070  prlngsym  29301  prlngpln3  29309  vtxdgoddnumeven  30016  ex-dif  30906  ococi  31889  orthin  31930  lediri  32021  pjoml2i  32069  pjoml4i  32071  cmcmlem  32075  cmbr3i  32084  cmm2i  32091  cm0  32093  fh1  32102  fh2  32103  cm2j  32104  qlaxr3i  32120  pjclem2  32680  stm1ri  32728  golem1  32755  dmdbr5  32792  mddmd2  32793  cvmdi  32808  mdsldmd1i  32815  csmdsymi  32818  mdexchi  32819  cvexchi  32853  atssma  32862  atomli  32866  atoml2i  32867  atordi  32868  atcvatlem  32869  chirredlem1  32874  chirredlem2  32875  chirredlem3  32876  atcvat4i  32881  atabsi  32885  mdsymlem1  32887  dmdbr6ati  32907  cdj3lem3  32922  inin  32994  difuncomp  33030  iundisj2f  33066  disjunsn  33070  imadifxp  33077  fnresin  33100  mptiffisupp  33168  mptprop  33173  df1stres  33179  df2ndres  33180  iocinif  33255  difioo  33256  fzodif1  33266  iundisj2fi  33271  xrge00  33457  symgcom  33526  cycpm2tr  33562  cycpmco2f1  33567  xrge0slmod  33791  oppr2idl  33891  ufdprmidl  33954  1arithufdlem4  33960  psrbasfsupp  34024  lindsun  34138  fldexttr  34171  lmxrge0  34465  esumrnmpt2  34581  esumpfinvallem  34587  ldgenpisyslem1  34677  ldgenpisys  34680  measxun2  34724  measunl  34730  carsgclctunlem1  34831  carsgclctunlem2  34833  eulerpartlemt  34885  eulerpartgbij  34886  probmeasb  34944  bayesth  34953  ballotlemfp1  35006  ballotlemfval0  35010  signstres  35086  hashreprin  35131  reprfz1  35135  chtvalz  35140  breprexpnat  35145  subfacp1lem3  35764  subfacp1lem5  35766  pconnconn  35813  cvmscld  35855  cvmsss2  35856  satef  35998  satefvfmla0  36000  mrsubvrs  36104  cldbnd  36948  bj-inrab3  37676  bj-2upln1upl  37771  bj-sscon  37776  bj-rest0  37846  bj-0int  37854  bj-ismooredr2  37863  icoreclin  38114  fin2so  38364  ptrest  38371  poimirlem3  38375  poimirlem11  38383  poimirlem12  38384  poimirlem13  38385  poimirlem14  38386  poimirlem15  38387  poimirlem18  38390  poimirlem21  38393  poimirlem22  38394  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  cnambfre  38420  asindmre  38455  dvasin  38456  dvreasin  38458  dvreacos  38459  sstotbnd2  38527  bndss  38539  inres2  38998  disjressuc2  39162  redundss3  39463  l1cvat  39931  pmod2iN  40725  pmodN  40726  pmodl42N  40727  osumcllem3N  40834  osumcllem4N  40835  dihmeetlem19N  42201  dihmeetALTN  42203  readvrec2  43239  elrfi  43542  diophrw  43607  eldioph2lem1  43608  eldioph2lem2  43609  diophin  43620  diophren  43657  dnwech  43892  fnwe2lem2  43895  kelac2lem  43908  kelac2  43909  lmhmlnmsplit  43931  pwssplit4  43933  pwfi2f1o  43940  proot1hash  44039  naddov4  44227  rp-fakeuninass  44359  elcnvcnvintab  44425  relintab  44426  elcnvcnvlem  44442  conrel1d  44506  dfrcl2  44517  iunrelexp0  44545  ntrk0kbimka  44882  hashnzfz  45147  zfregs2VD  45666  iunconnlem2  45760  ssinss2d  45897  restuni4  45956  restuni6  45957  restsubel  45988  iccdifioo  46348  uzinico2  46394  sumnnodd  46463  cncfuni  46717  fouriersw  47062  saliinclf  47157  iundjiunlem  47290  iundjiun  47291  caragenuncllem  47343  caragendifcl  47345  hoidmvlelem2  47427  smflimlem1  47602  3f1oss1  47966  perfectALTVlem2  48641  rngchomrnghmresALTV  49197  rngcrescrhmALTV  49198  rhmsubcALTVlem3  49201  rhmsubcALTVlem4  49202  resinsn  49801  resinsnALT  49802  tposrescnv  49808  opndisj  49832  restclssep  49845  seposep  49855  iscnrm3rlem3  49871  iscnrm3rlem8  49876  oppczeroo  50166