Theorem eqss 3240

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

Assertion

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

Proof of Theorem eqss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1533	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2223	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		ssalel 3213	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		ssalel 3213	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 460	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200   ⊆ wss 3198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqssi  3241  eqssd  3242  sseq1  3248  sseq2  3249  eqimss  3279  ssrabeq  3312  uneqin  3456  ss0b  3532  vss  3540  sssnm  3835  unidif  3923  ssunieq  3924  iuneq1  3981  iuneq2  3984  iunxdif2  4017  ssext  4311  pweqb  4313  eqopab2b  4372  pwunim  4381  soeq2  4411  iunpw  4575  ordunisuc2r  4610  tfi  4678  eqrel  4813  eqrelrel  4825  coeq1  4885  coeq2  4886  cnveq  4902  dmeq  4929  relssres  5049  xp11m  5173  xpcanm  5174  xpcan2m  5175  ssrnres  5177  fnres  5446  eqfnfv3  5742  fneqeql2  5752  fconst4m  5869  f1imaeq  5911  eqoprab2b  6074  fo1stresm  6319  fo2ndresm  6320  nnacan  6675  nnmcan  6682  ixpeq2  6876  sbthlemi3  7152  wrdeq  11128  isprm2  12682  lssle0  14379  bastop1  14800  epttop  14807  opnneiid  14881  cnntr  14942  metequiv  15212  bj-sseq  16338  bdeq0  16412  bdvsn  16419  bdop  16420  bdeqsuc  16426  bj-om  16482