Theorem incom 4230

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  {crab 3443   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444  df-in 3983

This theorem is referenced by:  ineqcom  4231  ineqcomi  4232  ineq2  4235  sseqin2  4244  in12  4250  in32  4251  in13  4252  in31  4253  inss2  4259  sslin  4264  inss  4268  dfss7  4270  indif1  4301  indifcom  4302  indir  4305  indifdir  4314  dfsymdif3  4325  dfrab2  4339  0in  4420  disjr  4474  disjdifr  4496  difdifdir  4515  uneqdifeq  4516  disjtp2  4741  iinrab2  5093  iunin1  5095  iinin1  5102  riinn0  5106  disjprg  5162  disjxun  5164  inex2  5336  inex2g  5338  rescom  6032  resindm  6059  resdmdfsn  6060  resopab  6063  imadisj  6109  intirr  6150  djudisj  6198  imainrect  6212  dmresv  6231  resdmres  6263  coeq0  6286  dfpred3  6343  predres  6371  frpoind  6374  wfiOLD  6383  ordtri3or  6427  fnresdisj  6700  fnimaeq0  6713  resasplit  6791  fresaun  6792  fresaunres2  6793  fresaunres1  6794  f0rn0  6806  fvun2  7014  rescnvimafod  7107  fveqressseq  7113  ressnop0  7187  fninfp  7208  fsnunfv  7221  orduniss2  7869  offres  8024  curry1  8145  curry2  8148  fpar  8157  fprlem1  8341  wfrlem5OLD  8369  smores3  8409  oacomf1o  8621  domunsncan  9138  phplem2OLD  9281  dif1ennnALT  9339  domunfican  9389  marypha1lem  9502  zfregfr  9674  epfrs  9800  zfregs2  9802  frind  9819  frrlem15  9826  djuin  9987  tskwe  10019  dfac8b  10100  ac10ct  10103  kmlem11  10230  kmlem12  10231  djucomen  10247  onadju  10263  ackbij1lem14  10301  ackbij1lem16  10303  fin23lem26  10394  fin23lem19  10405  fin23lem30  10411  isf32lem4  10425  isf34lem7  10448  isf34lem6  10449  axdc3lem4  10522  brdom7disj  10600  brdom6disj  10601  fpwwe2lem12  10711  fzpreddisj  13633  fzdifsuc  13644  fseq1p1m1  13658  prinfzo0  13755  hashun3  14433  hashbclem  14501  hash7g  14535  xpcoidgend  15024  cotr2  15026  limsupgle  15523  prmreclem2  16964  setsdm  17217  ressinbas  17304  wunress  17309  wunressOLD  17310  mreexexlem2d  17703  oppcinv  17841  cnvps  18648  pmtrmvd  19498  lsmmod2  19718  lsmdisj3  19725  lsmdisjr  19726  lsmdisj2r  19727  lsmdisj3r  19728  lsmdisj2a  19729  lsmdisj2b  19730  lsmdisj3a  19731  lsmdisj3b  19732  subgdisj2  19734  pj2f  19740  pj1id  19741  frgpuplem  19814  gsummptfzsplitl  19975  dprd2da  20086  dmdprdsplit2lem  20089  dmdprdsplit2  20090  pgpfaclem1  20125  rnghmsscmap2  20651  rnghmsubcsetclem1  20653  rnghmsubcsetc  20655  rngccat  20656  rngcid  20657  rngcifuestrc  20661  funcrngcsetc  20662  rhmsscmap2  20680  rhmsubcsetclem1  20682  rhmsubcsetc  20684  ringccat  20685  ringcid  20686  rhmsscrnghm  20687  rhmsubcrngclem1  20688  rhmsubcrngc  20690  rngcresringcat  20691  funcringcsetc  20696  rngcrescrhm  20706  rhmsubclem3  20709  rhmsubc  20711  lmhmlsp  21071  cnfldfunALTOLDOLD  21416  psgndiflemB  21641  pjpm  21751  ltbwe  22085  psrbag0  22109  elcls  23102  mretopd  23121  restin  23195  restcld  23201  resstopn  23215  lecldbas  23248  nrmsep  23386  isreg2  23406  ordthaus  23413  cmpsublem  23428  cmpsub  23429  hauscmplem  23435  bwth  23439  iunconn  23457  cldllycmp  23524  kgentopon  23567  llycmpkgen2  23579  1stckgen  23583  txkgen  23681  kqcldsat  23762  regr1lem2  23769  fbun  23869  fin1aufil  23961  fclsfnflim  24056  ustexsym  24245  restutopopn  24268  ustuqtop5  24275  ressuss  24292  metreslem  24393  blcld  24539  ressxms  24559  ressms  24560  reconn  24869  metdseq0  24895  metnrmlem3  24902  unmbl  25591  volun  25599  iundisj2  25603  icombl  25618  ioombl  25619  uniioombllem2  25637  uniioombllem4  25640  dyaddisjlem  25649  dyaddisj  25650  mbfconstlem  25681  mbfeqalem2  25696  ismbf3d  25708  itg1addlem5  25755  itgsplitioo  25893  lhop  26075  vieta1lem2  26371  xrlimcnp  27029  perfectlem2  27292  rplogsum  27589  nosupbnd2lem1  27778  sltlpss  27963  slelss  27964  perpcom  28739  vtxdgoddnumeven  29589  ex-dif  30455  ococi  31437  orthin  31478  lediri  31569  pjoml2i  31617  pjoml4i  31619  cmcmlem  31623  cmbr3i  31632  cmm2i  31639  cm0  31641  fh1  31650  fh2  31651  cm2j  31652  qlaxr3i  31668  pjclem2  32228  stm1ri  32276  golem1  32303  dmdbr5  32340  mddmd2  32341  cvmdi  32356  mdsldmd1i  32363  csmdsymi  32366  mdexchi  32367  cvexchi  32401  atssma  32410  atomli  32414  atoml2i  32415  atordi  32416  atcvatlem  32417  chirredlem1  32422  chirredlem2  32423  chirredlem3  32424  atcvat4i  32429  atabsi  32433  mdsymlem1  32435  dmdbr6ati  32455  cdj3lem3  32470  inin  32545  difuncomp  32576  iundisj2f  32612  disjunsn  32616  imadifxp  32623  fnresin  32645  mptiffisupp  32705  mptprop  32710  df1stres  32715  df2ndres  32716  padct  32733  iocinif  32786  difioo  32787  fzodif1  32798  iundisj2fi  32802  xrge00  32998  symgcom  33076  cycpm2tr  33112  cycpmco2f1  33117  xrge0slmod  33341  ssdifidlprm  33451  oppr2idl  33479  ufdprmidl  33534  1arithufdlem4  33540  lindsun  33638  fldexttr  33671  lmxrge0  33898  esumrnmpt2  34032  esumpfinvallem  34038  ldgenpisyslem1  34127  ldgenpisys  34130  measxun2  34174  measunl  34180  carsgclctunlem1  34282  carsgclctunlem2  34284  eulerpartlemt  34336  eulerpartgbij  34337  probmeasb  34395  bayesth  34404  ballotlemfp1  34456  ballotlemfval0  34460  signstres  34552  hashreprin  34597  reprfz1  34601  chtvalz  34606  breprexpnat  34611  f1resrcmplf1d  35063  f1resfz0f1d  35081  subfacp1lem3  35150  subfacp1lem5  35152  pconnconn  35199  cvmscld  35241  cvmsss2  35242  satef  35384  satefvfmla0  35386  mrsubvrs  35490  cldbnd  36292  bj-inrab3  36895  bj-2upln1upl  36990  bj-sscon  36995  bj-rest0  37059  bj-0int  37067  bj-ismooredr2  37076  icoreclin  37323  fin2so  37567  ptrest  37579  poimirlem3  37583  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  cnambfre  37628  asindmre  37663  dvasin  37664  dvreasin  37666  dvreacos  37667  sstotbnd2  37734  bndss  37746  inres2  38201  disjressuc2  38344  redundss3  38584  l1cvat  39011  pmod2iN  39806  pmodN  39807  pmodl42N  39808  osumcllem3N  39915  osumcllem4N  39916  dihmeetlem19N  41282  dihmeetALTN  41284  metakunt18  42179  elrfi  42650  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  diophin  42728  diophren  42769  dnwech  43005  fnwe2lem2  43008  kelac2lem  43021  kelac2  43022  lmhmlnmsplit  43044  pwssplit4  43046  pwfi2f1o  43053  proot1hash  43156  naddov4  43345  rp-fakeuninass  43478  elcnvcnvintab  43544  relintab  43545  elcnvcnvlem  43561  conrel1d  43625  dfrcl2  43636  iunrelexp0  43664  ntrk0kbimka  44001  hashnzfz  44289  zfregs2VD  44812  iunconnlem2  44906  ssinss2d  44962  restuni4  45023  restuni6  45024  restsubel  45058  iccdifioo  45433  uzinico2  45480  sumnnodd  45551  limsupvaluz  45629  cncfuni  45807  fouriersw  46152  saliinclf  46247  iundjiunlem  46380  iundjiun  46381  caragenuncllem  46433  caragendifcl  46435  hoidmvlelem2  46517  smflimlem1  46692  3f1oss1  46990  perfectALTVlem2  47596  rngchomrnghmresALTV  48002  rngcrescrhmALTV  48003  rhmsubcALTVlem3  48006  rhmsubcALTVlem4  48007  opndisj  48582  restclssep  48595  seposep  48605  iscnrm3rlem3  48622  iscnrm3rlem8  48627