Theorem cleqcom 1103

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41.

Assertion

Ref	Expression
cleqcom	|- (A = B <-> B = A)

Proof of Theorem cleqcom

Step	Hyp	Ref	Expression
1		bicom 398	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	bial 695	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 1098	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 1098	. 2 |- (B = A <-> A.x(x e. B <-> x e. A))
5	2, 3, 4	3bitr4 158	1 |- (A = B <-> B = A)

Syntax hints:   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092

This theorem is referenced by:  cleqcoms 1104  cleqcomi 1105  cleqcomd 1106  cleq2 1110  cleqabr 1175  necom 1198  gencbvex 1372  eqvinc 1407  sbcco2 1449  dfss 1493  sspsstri 1572  ssequn1 1628  0pss 1730  disj4 1737  ssnelpss 1751  preqr1 1872  0nep0 1887  dtru 1889  copsexg 1902  copsex4g 1904  opprc1b 1906  moop2 1910  opthwiener 1914  euuni 1954  opabid 2099  ordtri3or 2230  ordtri2 2233  onmindif2 2313  ordtri2or 2328  orduniorsuc 2337  suc11 2341  on0eqelt 2370  snsn0non 2371  opelxp 2452  opthprc 2457  elxp3 2460  cbvop 2473  dmopab2 2541  dmi 2545  rncoeq 2574  iss 2599  intirr 2628  cnvi 2634  coi1 2665  fcoi1 2765  fvprc 2829  fnopabfv 2858  fniunfv 2860  fnsnfv 2861  dmfco 2864  fvco 2865  fvopabn 2873  elrnopab 2884  funopfv 2886  fconstfv 2903  fvclss 2907  f1fv 2916  f1oiso 2942  rdglim2 2987  tz7.48lem 2993  eloprabg 3035  elrnoprab 3054  1st2val 3097  oawordeulem 3156  erthdmr 3221  0nelqs 3234  qsid 3237  brecop 3242  ecopoprsym 3246  map0 3268  nneneq 3408  unfilem1 3438  suc11reg 3456  inf3lem2 3465  inf3lem6 3469  aceq5lem2 3559  aceq5lem3 3560  aceq5lem4 3561  aceq5 3563  kmlem3 3582  kmlem4 3583  kmlem15 3594  unxpdomlem 3649  isinfcard 3692  cfsuc 3709  cdacomen 3724  ordpipq 3850  prnmadd 3894  psslinpr 3929  ltexprlem4 3939  suplem2pr 3956  ltsrpr 3980  mulgt0sr 4008  elreal 4044  negcon1 4165  negcon2 4166  negcon2t 4168  divneq0bt 4230  rec11i 4261  leloet 4284  lesubadd2 4318  add20 4329  leneg 4331  negne0 4379  divge0 4392  lerec 4411  nngt1ne1t 4440  arch 4521  nn0ge0i 4559  elnnz 4572  elnn0z 4574  elznn0 4576  nn0subt 4587  elnn0nn 4593  zltp1let 4597  zqt 4632  nn0opth 4724  sqr2irrlem4 4780  cjre 4811  absgt0 4842  nn0ennn 4925  znnen 4930  hvsubadd 5038  his6 5057  norm-it 5080  chocuni 5179  omlsilem 5249  shmods 5363  chnle 5406  pjoml3 5496  cmbr2 5505  pjin2 5647  pjin3 5648  pjnel 5665  large 5700  cvnbtwn3t 5720  cvnbtwn4t 5721  atnem0 5766  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org