Theorem incom 4202

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  {crab 3430   ∩ cin 3948

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-rab 3431  df-in 3956

This theorem is referenced by:  ineqcom  4203  ineqcomi  4204  ineq2  4207  sseqin2  4216  in12  4221  in32  4222  in13  4223  in31  4224  inss2  4230  sslin  4235  inss  4239  dfss7  4241  indif1  4272  indifcom  4273  indir  4276  indifdir  4285  dfsymdif3  4297  dfrab2  4311  0in  4394  disjr  4450  disjdifr  4473  difdifdir  4492  uneqdifeq  4493  disjtp2  4721  iinrab2  5074  iunin1  5076  iinin1  5083  riinn0  5087  disjprgw  5144  disjprg  5145  disjxun  5147  inex2  5319  inex2g  5321  rescom  6008  resindm  6031  resdmdfsn  6032  resopab  6035  imadisj  6080  intirr  6120  djudisj  6167  imainrect  6181  dmresv  6200  resdmres  6232  coeq0  6255  dfpred3  6312  predres  6341  frpoind  6344  wfiOLD  6353  ordtri3or  6397  fnresdisj  6671  fnimaeq0  6684  resasplit  6762  fresaun  6763  fresaunres2  6764  fresaunres1  6765  f0rn0  6777  fvun2  6984  rescnvimafod  7076  fveqressseq  7082  ressnop0  7154  fninfp  7175  fsnunfv  7188  orduniss2  7825  offres  7974  curry1  8094  curry2  8097  fpar  8106  fprlem1  8289  wfrlem5OLD  8317  smores3  8357  oacomf1o  8569  domunsncan  9076  phplem2OLD  9222  pssnnOLD  9269  dif1ennnALT  9281  domunfican  9324  marypha1lem  9432  zfregfr  9604  epfrs  9730  zfregs2  9732  frind  9749  frrlem15  9756  djuin  9917  tskwe  9949  dfac8b  10030  ac10ct  10033  kmlem11  10159  kmlem12  10160  djucomen  10176  onadju  10192  ackbij1lem14  10232  ackbij1lem16  10234  fin23lem26  10324  fin23lem19  10335  fin23lem30  10341  isf32lem4  10355  isf34lem7  10378  isf34lem6  10379  axdc3lem4  10452  brdom7disj  10530  brdom6disj  10531  fpwwe2lem12  10641  fzpreddisj  13556  fzdifsuc  13567  fseq1p1m1  13581  prinfzo0  13677  hashun3  14350  hashbclem  14417  xpcoidgend  14928  cotr2  14930  limsupgle  15427  prmreclem2  16856  setsdm  17109  ressinbas  17196  wunress  17201  wunressOLD  17202  mreexexlem2d  17595  oppcinv  17733  cnvps  18537  pmtrmvd  19367  lsmmod2  19587  lsmdisj3  19594  lsmdisjr  19595  lsmdisj2r  19596  lsmdisj3r  19597  lsmdisj2a  19598  lsmdisj2b  19599  lsmdisj3a  19600  lsmdisj3b  19601  subgdisj2  19603  pj2f  19609  pj1id  19610  frgpuplem  19683  gsummptfzsplitl  19844  dprd2da  19955  dmdprdsplit2lem  19958  dmdprdsplit2  19959  pgpfaclem1  19994  lmhmlsp  20806  cnfldfunALTOLD  21160  psgndiflemB  21374  pjpm  21484  ltbwe  21820  psrbag0  21844  elcls  22799  mretopd  22818  restin  22892  restcld  22898  resstopn  22912  lecldbas  22945  nrmsep  23083  isreg2  23103  ordthaus  23110  cmpsublem  23125  cmpsub  23126  hauscmplem  23132  bwth  23136  iunconn  23154  cldllycmp  23221  kgentopon  23264  llycmpkgen2  23276  1stckgen  23280  txkgen  23378  kqcldsat  23459  regr1lem2  23466  fbun  23566  fin1aufil  23658  fclsfnflim  23753  ustexsym  23942  restutopopn  23965  ustuqtop5  23972  ressuss  23989  metreslem  24090  blcld  24236  ressxms  24256  ressms  24257  reconn  24566  metdseq0  24592  metnrmlem3  24599  unmbl  25288  volun  25296  iundisj2  25300  icombl  25315  ioombl  25316  uniioombllem2  25334  uniioombllem4  25337  dyaddisjlem  25346  dyaddisj  25347  mbfconstlem  25378  mbfeqalem2  25393  ismbf3d  25405  itg1addlem5  25452  itgsplitioo  25589  lhop  25767  tdeglem4OLD  25812  vieta1lem2  26058  xrlimcnp  26707  perfectlem2  26967  rplogsum  27264  nosupbnd2lem1  27452  sltlpss  27636  slelss  27637  perpcom  28229  vtxdgoddnumeven  29075  ex-dif  29941  ococi  30923  orthin  30964  lediri  31055  pjoml2i  31103  pjoml4i  31105  cmcmlem  31109  cmbr3i  31118  cmm2i  31125  cm0  31127  fh1  31136  fh2  31137  cm2j  31138  qlaxr3i  31154  pjclem2  31714  stm1ri  31762  golem1  31789  dmdbr5  31826  mddmd2  31827  cvmdi  31842  mdsldmd1i  31849  csmdsymi  31852  mdexchi  31853  cvexchi  31887  atssma  31896  atomli  31900  atoml2i  31901  atordi  31902  atcvatlem  31903  chirredlem1  31908  chirredlem2  31909  chirredlem3  31910  atcvat4i  31915  atabsi  31919  mdsymlem1  31921  dmdbr6ati  31941  cdj3lem3  31956  inin  32018  difuncomp  32050  iundisj2f  32086  disjunsn  32090  imadifxp  32097  fnresin  32115  mptiffisupp  32180  mptprop  32185  df1stres  32190  df2ndres  32191  padct  32209  iocinif  32257  difioo  32258  fzodif1  32269  iundisj2fi  32273  xrge00  32452  symgcom  32512  cycpm2tr  32546  cycpmco2f1  32551  xrge0slmod  32731  oppr2idl  32872  lindsun  32996  fldexttr  33023  lmxrge0  33228  esumrnmpt2  33362  esumpfinvallem  33368  ldgenpisyslem1  33457  ldgenpisys  33460  measxun2  33504  measunl  33510  carsgclctunlem1  33612  carsgclctunlem2  33614  eulerpartlemt  33666  eulerpartgbij  33667  probmeasb  33725  bayesth  33734  ballotlemfp1  33786  ballotlemfval0  33790  signstres  33882  hashreprin  33928  reprfz1  33932  chtvalz  33937  breprexpnat  33942  f1resrcmplf1d  34386  f1resfz0f1d  34399  subfacp1lem3  34469  subfacp1lem5  34471  pconnconn  34518  cvmscld  34560  cvmsss2  34561  satef  34703  satefvfmla0  34705  mrsubvrs  34809  cldbnd  35516  bj-inrab3  36114  bj-2upln1upl  36210  bj-sscon  36215  bj-rest0  36279  bj-0int  36287  bj-ismooredr2  36296  icoreclin  36543  fin2so  36780  ptrest  36792  poimirlem3  36796  poimirlem11  36804  poimirlem12  36805  poimirlem13  36806  poimirlem14  36807  poimirlem15  36808  poimirlem18  36811  poimirlem21  36814  poimirlem22  36815  mblfinlem3  36832  mblfinlem4  36833  ismblfin  36834  cnambfre  36841  asindmre  36876  dvasin  36877  dvreasin  36879  dvreacos  36880  sstotbnd2  36947  bndss  36959  inres2  37417  disjressuc2  37563  redundss3  37803  l1cvat  38230  pmod2iN  39025  pmodN  39026  pmodl42N  39027  osumcllem3N  39134  osumcllem4N  39135  dihmeetlem19N  40501  dihmeetALTN  40503  metakunt18  41310  elrfi  41736  diophrw  41801  eldioph2lem1  41802  eldioph2lem2  41803  diophin  41814  diophren  41855  dnwech  42094  fnwe2lem2  42097  kelac2lem  42110  kelac2  42111  lmhmlnmsplit  42133  pwssplit4  42135  pwfi2f1o  42142  proot1hash  42246  naddov4  42437  rp-fakeuninass  42571  elcnvcnvintab  42637  relintab  42638  elcnvcnvlem  42654  conrel1d  42718  dfrcl2  42729  iunrelexp0  42757  ntrk0kbimka  43094  hashnzfz  43383  zfregs2VD  43906  iunconnlem2  44000  ssinss2d  44050  restuni4  44113  restuni6  44114  restsubel  44150  iccdifioo  44528  uzinico2  44575  sumnnodd  44646  limsupvaluz  44724  cncfuni  44902  fouriersw  45247  saliinclf  45342  iundjiunlem  45475  iundjiun  45476  caragenuncllem  45528  caragendifcl  45530  hoidmvlelem2  45612  smflimlem1  45787  perfectALTVlem2  46690  rnghmsscmap2  46961  rnghmsubcsetclem1  46963  rnghmsubcsetc  46965  rngccat  46966  rngcid  46967  rngchomrnghmresALTV  46984  rngcifuestrc  46985  funcrngcsetc  46986  rhmsscmap2  47007  rhmsubcsetclem1  47009  rhmsubcsetc  47011  ringccat  47012  ringcid  47013  rhmsscrnghm  47014  rhmsubcrngclem1  47015  rhmsubcrngc  47017  rngcresringcat  47018  funcringcsetc  47023  rngcrescrhm  47073  rhmsubclem3  47076  rhmsubc  47078  rngcrescrhmALTV  47091  rhmsubcALTVlem3  47094  rhmsubcALTVlem4  47095  opndisj  47624  restclssep  47637  seposep  47647  iscnrm3rlem3  47664  iscnrm3rlem8  47669