Theorem incom 4168

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 3412	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
2		dfin5 3919	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
3		dfin5 3919	. 2 ⊢ (𝐵 ∩ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
4	1, 2, 3	3eqtr4i 2762	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3402   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3403  df-in 3918

This theorem is referenced by:  ineqcom  4169  ineqcomi  4170  ineq2  4173  sseqin2  4182  in12  4188  in32  4189  in13  4190  in31  4191  inss2  4197  sslin  4202  inss  4207  dfss7  4210  indif1  4241  indifcom  4242  indir  4245  indifdir  4254  dfsymdif3  4265  dfrab2  4279  0in  4356  disjr  4410  disjdifr  4432  difdifdir  4451  uneqdifeq  4452  disjtp2  4676  iinrab2  5029  iunin1  5031  iinin1  5038  riinn0  5042  disjprg  5098  disjxun  5100  inex2  5268  inex2g  5270  rescom  5962  resindm  5990  resdmdfsn  5991  resopab  5994  imadisj  6040  intirr  6079  djudisj  6128  imainrect  6142  dmresv  6161  resdmres  6193  coeq0  6216  dfpred3  6273  predres  6300  frpoind  6303  ordtri3or  6352  fnresdisj  6620  fnimaeq0  6633  resasplit  6712  fresaun  6713  fresaunres2  6714  fresaunres1  6715  f0rn0  6727  fvun2  6935  rescnvimafod  7027  fveqressseq  7033  ressnop0  7107  fninfp  7130  fsnunfv  7143  orduniss2  7788  offres  7941  curry1  8060  curry2  8063  fpar  8072  fprlem1  8256  smores3  8299  oacomf1o  8506  domunsncan  9018  dif1ennnALT  9198  domunfican  9248  marypha1lem  9360  zfregfr  9534  epfrs  9660  zfregs2  9662  frind  9679  frrlem15  9686  djuin  9847  tskwe  9879  dfac8b  9960  ac10ct  9963  kmlem11  10090  kmlem12  10091  djucomen  10107  onadju  10123  ackbij1lem14  10161  ackbij1lem16  10163  fin23lem26  10254  fin23lem19  10265  fin23lem30  10271  isf32lem4  10285  isf34lem7  10308  isf34lem6  10309  axdc3lem4  10382  brdom7disj  10460  brdom6disj  10461  fpwwe2lem12  10571  fzpreddisj  13510  fzdifsuc  13521  fseq1p1m1  13535  prinfzo0  13635  hashun3  14325  hashbclem  14393  hash7g  14427  xpcoidgend  14917  cotr2  14919  limsupgle  15419  prmreclem2  16864  setsdm  17116  ressinbas  17191  wunress  17195  mreexexlem2d  17586  oppcinv  17722  cnvps  18519  pmtrmvd  19370  lsmmod2  19590  lsmdisj3  19597  lsmdisjr  19598  lsmdisj2r  19599  lsmdisj3r  19600  lsmdisj2a  19601  lsmdisj2b  19602  lsmdisj3a  19603  lsmdisj3b  19604  subgdisj2  19606  pj2f  19612  pj1id  19613  frgpuplem  19686  gsummptfzsplitl  19847  dprd2da  19958  dmdprdsplit2lem  19961  dmdprdsplit2  19962  pgpfaclem1  19997  rnghmsscmap2  20549  rnghmsubcsetclem1  20551  rnghmsubcsetc  20553  rngccat  20554  rngcid  20555  rngcifuestrc  20559  funcrngcsetc  20560  rhmsscmap2  20578  rhmsubcsetclem1  20580  rhmsubcsetc  20582  ringccat  20583  ringcid  20584  rhmsscrnghm  20585  rhmsubcrngclem1  20586  rhmsubcrngc  20588  rngcresringcat  20589  funcringcsetc  20594  rngcrescrhm  20604  rhmsubclem3  20607  rhmsubc  20609  lmhmlsp  20988  psgndiflemB  21542  pjpm  21650  ltbwe  21984  psrbag0  22002  elcls  22993  mretopd  23012  restin  23086  restcld  23092  resstopn  23106  lecldbas  23139  nrmsep  23277  isreg2  23297  ordthaus  23304  cmpsublem  23319  cmpsub  23320  hauscmplem  23326  bwth  23330  iunconn  23348  cldllycmp  23415  kgentopon  23458  llycmpkgen2  23470  1stckgen  23474  txkgen  23572  kqcldsat  23653  regr1lem2  23660  fbun  23760  fin1aufil  23852  fclsfnflim  23947  ustexsym  24136  restutopopn  24159  ustuqtop5  24166  ressuss  24183  metreslem  24283  blcld  24426  ressxms  24446  ressms  24447  reconn  24750  metdseq0  24776  metnrmlem3  24783  unmbl  25471  volun  25479  iundisj2  25483  icombl  25498  ioombl  25499  uniioombllem2  25517  uniioombllem4  25520  dyaddisjlem  25529  dyaddisj  25530  mbfconstlem  25561  mbfeqalem2  25576  ismbf3d  25588  itg1addlem5  25634  itgsplitioo  25772  lhop  25954  vieta1lem2  26252  xrlimcnp  26911  perfectlem2  27174  rplogsum  27471  nosupbnd2lem1  27660  sltlpss  27857  slelss  27858  perpcom  28693  vtxdgoddnumeven  29534  ex-dif  30402  ococi  31384  orthin  31425  lediri  31516  pjoml2i  31564  pjoml4i  31566  cmcmlem  31570  cmbr3i  31579  cmm2i  31586  cm0  31588  fh1  31597  fh2  31598  cm2j  31599  qlaxr3i  31615  pjclem2  32175  stm1ri  32223  golem1  32250  dmdbr5  32287  mddmd2  32288  cvmdi  32303  mdsldmd1i  32310  csmdsymi  32313  mdexchi  32314  cvexchi  32348  atssma  32357  atomli  32361  atoml2i  32362  atordi  32363  atcvatlem  32364  chirredlem1  32369  chirredlem2  32370  chirredlem3  32371  atcvat4i  32376  atabsi  32380  mdsymlem1  32382  dmdbr6ati  32402  cdj3lem3  32417  inin  32495  difuncomp  32532  iundisj2f  32569  disjunsn  32573  imadifxp  32580  fnresin  32600  mptiffisupp  32666  mptprop  32671  df1stres  32677  df2ndres  32678  padct  32693  iocinif  32754  difioo  32755  fzodif1  32765  iundisj2fi  32770  xrge00  32998  symgcom  33055  cycpm2tr  33091  cycpmco2f1  33096  xrge0slmod  33312  ssdifidlprm  33422  oppr2idl  33450  ufdprmidl  33505  1arithufdlem4  33511  lindsun  33614  fldexttr  33647  lmxrge0  33935  esumrnmpt2  34051  esumpfinvallem  34057  ldgenpisyslem1  34146  ldgenpisys  34149  measxun2  34193  measunl  34199  carsgclctunlem1  34301  carsgclctunlem2  34303  eulerpartlemt  34355  eulerpartgbij  34356  probmeasb  34414  bayesth  34423  ballotlemfp1  34476  ballotlemfval0  34480  signstres  34559  hashreprin  34604  reprfz1  34608  chtvalz  34613  breprexpnat  34618  f1resrcmplf1d  35070  f1resfz0f1d  35094  subfacp1lem3  35162  subfacp1lem5  35164  pconnconn  35211  cvmscld  35253  cvmsss2  35254  satef  35396  satefvfmla0  35398  mrsubvrs  35502  cldbnd  36307  bj-inrab3  36910  bj-2upln1upl  37005  bj-sscon  37010  bj-rest0  37074  bj-0int  37082  bj-ismooredr2  37091  icoreclin  37338  fin2so  37594  ptrest  37606  poimirlem3  37610  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  cnambfre  37655  asindmre  37690  dvasin  37691  dvreasin  37693  dvreacos  37694  sstotbnd2  37761  bndss  37773  inres2  38227  disjressuc2  38367  redundss3  38612  l1cvat  39041  pmod2iN  39836  pmodN  39837  pmodl42N  39838  osumcllem3N  39945  osumcllem4N  39946  dihmeetlem19N  41312  dihmeetALTN  41314  readvrec2  42342  elrfi  42675  diophrw  42740  eldioph2lem1  42741  eldioph2lem2  42742  diophin  42753  diophren  42794  dnwech  43030  fnwe2lem2  43033  kelac2lem  43046  kelac2  43047  lmhmlnmsplit  43069  pwssplit4  43071  pwfi2f1o  43078  proot1hash  43177  naddov4  43365  rp-fakeuninass  43498  elcnvcnvintab  43564  relintab  43565  elcnvcnvlem  43581  conrel1d  43645  dfrcl2  43656  iunrelexp0  43684  ntrk0kbimka  44021  hashnzfz  44302  zfregs2VD  44823  iunconnlem2  44917  ssinss2d  45047  restuni4  45108  restuni6  45109  restsubel  45140  iccdifioo  45506  uzinico2  45552  sumnnodd  45621  limsupvaluz  45699  cncfuni  45877  fouriersw  46222  saliinclf  46317  iundjiunlem  46450  iundjiun  46451  caragenuncllem  46503  caragendifcl  46505  hoidmvlelem2  46587  smflimlem1  46762  3f1oss1  47069  perfectALTVlem2  47716  rngchomrnghmresALTV  48260  rngcrescrhmALTV  48261  rhmsubcALTVlem3  48264  rhmsubcALTVlem4  48265  resinsn  48853  resinsnALT  48854  tposrescnv  48860  opndisj  48884  restclssep  48897  seposep  48907  iscnrm3rlem3  48923  iscnrm3rlem8  48928  oppczeroo  49219