Theorem eqss 4024

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)

Assertion

Ref	Expression
eqss	⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Proof of Theorem eqss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1888	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2733	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3993	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3993	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 627	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976

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-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqssi  4025  eqssd  4026  sssseq  4027  sseq1  4034  sseq2  4035  ssrabeq  4107  dfpss3  4112  compleq  4175  uneqin  4308  rcompleq  4324  pssdifn0  4391  ss0b  4424  vss  4469  pwpw0  4838  sssn  4851  ssunsn  4853  unidif  4966  ssunieq  4967  uniintsn  5009  iuneq1  5031  iuneq2  5034  iunxdif2  5076  ssext  5474  pweqb  5476  eqopab2bw  5567  eqopab2b  5571  pwun  5591  soeq2  5630  eqrel  5808  eqrelrel  5821  coeq1  5882  coeq2  5883  cnveq  5898  dmeq  5928  relssres  6051  xp11  6206  ssrnres  6209  ordtri4  6432  oneqmini  6447  fnres  6707  eqfnfv3  7066  fneqeql2  7080  dff3  7134  fconst4  7251  f1imaeq  7302  eqoprab2bw  7520  eqoprab2b  7521  iunpw  7806  orduniorsuc  7866  tfi  7890  fo1stres  8056  fo2ndres  8057  wfrlem8OLD  8372  tz7.49  8501  oawordeulem  8610  nnacan  8684  nnmcan  8690  ixpeq2  8969  sbthlem3  9151  isinf  9323  isinfOLD  9324  ordunifi  9354  inficl  9494  rankr1c  9890  rankc1  9939  iscard  10044  iscard2  10045  carden2  10056  aleph11  10153  cardaleph  10158  alephinit  10164  dfac12a  10218  cflm  10319  cfslb2n  10337  dfacfin7  10468  wrdeq  14584  isumltss  15896  rpnnen2lem12  16273  isprm2  16729  mrcidb2  17676  smndex2dnrinv  18950  iscyggen2  19923  iscyg3  19928  lssle0  20971  islpir2  21363  iscss2  21727  ishil2  21762  bastop1  23021  epttop  23037  iscld4  23094  0ntr  23100  opnneiid  23155  isperf2  23181  cnntr  23304  ist1-3  23378  perfcls  23394  cmpfi  23437  isconn2  23443  dfconn2  23448  snfil  23893  filconn  23912  ufileu  23948  alexsubALTlem4  24079  metequiv  24543  eqscut2  27869  nbuhgr2vtx1edgblem  29386  iscplgr  29450  shlesb1i  31418  shle0  31474  orthin  31478  chcon2i  31496  chcon3i  31498  chlejb1i  31508  chabs2  31549  h1datomi  31613  cmbr4i  31633  osumcor2i  31676  pjjsi  31732  pjin2i  32225  stcltr2i  32307  mdbr2  32328  dmdbr2  32335  mdsl2i  32354  mdsl2bi  32355  mdslmd3i  32364  chrelat4i  32405  sumdmdlem2  32451  dmdbr5ati  32454  eqdif  32549  eqrelrd2  32638  rspsnasso  33381  dfon2lem9  35755  idsset  35854  fneval  36318  topdifinfeq  37316  equivtotbnd  37738  heiborlem10  37780  eqrel2  38255  relcnveq3  38277  relcnveq2  38279  cossssid  38423  elrelscnveq3  38447  elrelscnveq2  38449  pmap11  39719  dia11N  41005  dia2dimlem5  41025  dib11N  41117  dih11  41222  dihglblem6  41297  doch11  41330  mapd11  41596  mapdcnv11N  41616  sticksstones11  42113  isnacs2  42662  mrefg3  42664  onsupneqmaxlim0  43185  onsupnmax  43189  ontric3g  43484  rababg  43536  relnonrel  43549  uneqsn  43987  ntrk1k3eqk13  44012  ntrneineine1lem  44046  ntrneicls00  44051  ntrneixb  44057  ntrneik13  44060  ntrneix13  44061  joindm2  48648  meetdm2  48650