Theorem eqss 3954

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 1912	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2758	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3924	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3924	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 639	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  eqssi  3955  eqssd  3956  sssseq  3957  sseq1  3964  sseq2  3965  ssrabeq  4040  dfpss3  4045  compleq  4108  uneqin  4244  rcompleq  4260  pssdifn0  4324  ss0b  4358  vss  4403  pwpw0  4774  sssn  4787  ssunsn  4789  unidif  4903  ssunieq  4904  uniintsn  4945  iuneq1  4968  iuneq2  4971  iunxdif2  5013  ssext  5425  pweqb  5427  eqopab2bw  5523  eqopab2b  5527  pwun  5544  soeq2  5581  eqrel  5760  eqrelrel  5773  coeq1  5833  coeq2  5834  cnveq  5849  dmeq  5883  relssres  6011  xp11  6164  ssrnres  6167  ordtri4  6387  oneqmini  6403  fnres  6652  eqfnfv3  7017  fneqeql2  7032  dff3  7085  fconst4  7202  f1imaeq  7253  eqoprab2bw  7470  eqoprab2b  7471  iunpw  7758  orduniorsuc  7814  tfi  7837  fo1stres  8000  fo2ndres  8001  tz7.49  8420  oawordeulem  8527  nnacan  8602  nnmcan  8608  ixpeq2  8897  sbthlem3  9065  isinf  9213  ordunifi  9238  inficl  9373  rankr1c  9781  rankc1  9830  iscard  9949  iscard2  9950  carden2  9961  aleph11  10056  cardaleph  10061  alephinit  10067  dfac12a  10120  cflm  10221  cfslb2n  10240  dfacfin7  10371  wrdeq  14561  isumltss  15890  rpnnen2lem12  16269  isprm2  16728  mrcidb2  17662  smndex2dnrinv  18965  iscyggen2  19939  iscyg3  19944  lssle0  21037  islpir2  21455  iscss2  21793  ishil2  21826  bastop1  23107  epttop  23123  iscld4  23179  0ntr  23185  opnneiid  23240  isperf2  23266  cnntr  23389  ist1-3  23463  perfcls  23479  cmpfi  23522  isconn2  23528  dfconn2  23533  snfil  23978  filconn  23997  ufileu  24033  alexsubALTlem4  24164  metequiv  24623  eqcuts2  27933  nbuhgr2vtx1edgblem  29606  iscplgr  29670  shlesb1i  31643  shle0  31699  orthin  31703  chcon2i  31721  chcon3i  31723  chlejb1i  31733  chabs2  31774  h1datomi  31838  cmbr4i  31858  osumcor2i  31901  pjjsi  31957  pjin2i  32450  stcltr2i  32532  mdbr2  32553  dmdbr2  32560  mdsl2i  32579  mdsl2bi  32580  mdslmd3i  32589  chrelat4i  32630  sumdmdlem2  32676  dmdbr5ati  32679  eqdif  32771  eqrelrd2  32869  rspsnasso  33612  dfon2lem9  36147  idsset  36246  fneval  36720  topdifinfeq  37851  equivtotbnd  38284  heiborlem10  38326  eqrel2  38811  relcnveq3  38833  relcnveq2  38835  cossssid  39063  elrelscnveq3  39133  elrelscnveq2  39135  pmap11  40393  dia11N  41679  dia2dimlem5  41699  dib11N  41791  dih11  41896  dihglblem6  41971  doch11  42004  mapd11  42270  mapdcnv11N  42290  sticksstones11  42780  isnacs2  43294  mrefg3  43296  onsupneqmaxlim0  43808  onsupnmax  43812  ontric3g  44105  rababg  44157  relnonrel  44170  uneqsn  44608  ntrk1k3eqk13  44633  ntrneineine1lem  44667  ntrneicls00  44672  ntrneixb  44678  ntrneik13  44681  ntrneix13  44682  joindm2  49598  meetdm2  49600