Theorem eqcom 1474

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

Assertion

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

Proof of Theorem eqcom

Step	Hyp	Ref	Expression
1		bicom 519	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	albii 997	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 1468	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 1468	. 2 |- (B = A <-> A.x(x e. B <-> x e. A))
5	2, 3, 4	3bitr4 183	1 |- (A = B <-> B = A)

Syntax hints:   <-> wb 146  A.wal 952   = wceq 954   e. wcel 956

This theorem is referenced by:  eqcoms 1475  eqcomi 1476  eqcomd 1477  eqeq2 1481  eqtr2t 1490  eqtr3t 1491  abeq1 1566  necom 1633  gencbvex 1834  eqvinc 1879  reu7 1931  reu8 1932  sbcco2 1949  dfss 2050  sspsstri 2144  ssequn1 2196  disj4 2313  ssnelpss 2326  preqr1 2477  dtru 2767  copsexg 2787  copsex4g 2789  opprc1b 2791  opeqsn 2797  opeqpr 2798  opthwiener 2802  opabid 2805  euuni 2876  ordtri3or 2974  ordtri2 2977  onmindif2 3056  ordtri2or 3072  suc11 3088  on0eqelt 3119  snsn0non 3120  opelxp 3209  opthprc 3216  elxp3 3219  relop 3270  dmopab3 3317  dmi 3321  rncoeq 3359  iss 3389  intirr 3433  cnvi 3439  coi1 3502  cnvso 3515  fcoi1 3636  fvprc 3712  fnopabfv 3749  fnrnfv 3750  fvelrnb 3751  dfimafn2 3753  funimass4 3754  fnsnfv 3758  dmfco 3764  fvco 3765  fvopabn 3777  elrnopabg 3791  funfvop 3794  dffo4 3811  fconstfv 3840  fvclss 3846  funiunfv 3857  f1fv 3865  f1ocnvfv3 3874  f1oiso 3895  rdglim2 3940  tz7.48lem 3946  eloprabg 3998  oprvalelrn 4030  1st2val 4085  2nd2val 4086  dfoprab5 4105  elrnoprabg 4114  erthdmr 4274  0nelqs 4288  qsid 4291  brecop 4296  ecopoprsym 4300  nneneq 4498  unfilem1 4530  suc11reg 4585  inf3lem2 4594  inf3lem6 4598  aceq5lem2 4716  aceq5lem3 4717  aceq5 4720  kmlem15 4759  brdom7disj 4784  brdom6disj 4785  unxpdomlem 4823  isinfcard 4867  cfeq0 4894  cfsuc 4895  ordpipq 5036  prnmadd 5080  psslinpr 5115  ltexprlem4 5125  suplem2pr 5142  ltsrpr 5166  mulgt0sr 5194  elreal 5230  negcon1 5387  negcon2 5388  negcon1t 5390  negcon2t 5391  leloet 5499  xrleloet 5538  ngtmnftt 5548  lesubadd 5577  add20 5584  leneg 5586  divmul2t 5685  divne0bt 5699  rec11i 5741  conjmult 5761  negeq0t 5770  lerec 5836  arch 6026  elnn0z 6102  elznn0 6104  nn0subt 6116  elnn0nn 6126  zltp1let 6136  zqt 6206  snunioolem 6355  elfzp1 6450  fzneuzt 6458  nn0opth 6604  sqr2irrlem4 6665  cjreb 6724  absgt0 6786  leabst 6807  abssubne0t 6828  dffsum 6944  dfisum 7135  geoser 7177  reeff1o 7376  nn0ennn 7447  znnen 7453  istps2 7557  cnconst 7730  isgrp 7991  isgrp2i 8026  mulid 8084  nvsubadd 8227  cosh111lem3 8650  efif1lem7 8670  hvsubadd 8872  hiret 8899  hilid 8967  chocuni 9111  omlsilem 9182  shmods 9300  chcon1 9326  chnle 9346  pjoml3 9469  cmbr2 9479  adjsymt 9699  eigorth 9703  dfadj2 9752  adjval2t 9755  cnvadj 9756  dmadjrnb 9770  cnlnadjeu 9948  cnlnssadj 9951  adjbdlnt 9954  pjima 10042  pjin2 10059  pjin3 10060  large 10132  cvnbtwn3t 10153  cvnbtwn4t 10154  mddmd 10173  superpos 10218  atnem0 10241  sumdmdi 10278  sumdmdlem 10281  elo 10381  homcard 10462  cmpmon 10621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain