Theorem eqss 3195

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 1498	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2187	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3169	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3169	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 460	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  eqssi  3196  eqssd  3197  sseq1  3203  sseq2  3204  eqimss  3234  ssrabeq  3267  uneqin  3411  ss0b  3487  vss  3495  sssnm  3781  unidif  3868  ssunieq  3869  iuneq1  3926  iuneq2  3929  iunxdif2  3962  ssext  4251  pweqb  4253  eqopab2b  4311  pwunim  4318  soeq2  4348  iunpw  4512  ordunisuc2r  4547  tfi  4615  eqrel  4749  eqrelrel  4761  coeq1  4820  coeq2  4821  cnveq  4837  dmeq  4863  relssres  4981  xp11m  5105  xpcanm  5106  xpcan2m  5107  ssrnres  5109  fnres  5371  eqfnfv3  5658  fneqeql2  5668  fconst4m  5779  f1imaeq  5819  eqoprab2b  5977  fo1stresm  6216  fo2ndresm  6217  nnacan  6567  nnmcan  6574  ixpeq2  6768  sbthlemi3  7020  wrdeq  10939  isprm2  12258  lssle0  13871  bastop1  14262  epttop  14269  opnneiid  14343  cnntr  14404  metequiv  14674  bj-sseq  15354  bdeq0  15429  bdvsn  15436  bdop  15437  bdeqsuc  15443  bj-om  15499