Theorem eqss 3171

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1351   = wceq 1353   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  eqssi  3172  eqssd  3173  sseq1  3179  sseq2  3180  eqimss  3210  ssrabeq  3243  uneqin  3387  ss0b  3463  vss  3471  sssnm  3755  unidif  3842  ssunieq  3843  iuneq1  3900  iuneq2  3903  iunxdif2  3936  ssext  4222  pweqb  4224  eqopab2b  4280  pwunim  4287  soeq2  4317  iunpw  4481  ordunisuc2r  4514  tfi  4582  eqrel  4716  eqrelrel  4728  coeq1  4785  coeq2  4786  cnveq  4802  dmeq  4828  relssres  4946  xp11m  5068  xpcanm  5069  xpcan2m  5070  ssrnres  5072  fnres  5333  eqfnfv3  5616  fneqeql2  5626  fconst4m  5737  f1imaeq  5776  eqoprab2b  5933  fo1stresm  6162  fo2ndresm  6163  nnacan  6513  nnmcan  6520  ixpeq2  6712  sbthlemi3  6958  isprm2  12117  bastop1  13586  epttop  13593  opnneiid  13667  cnntr  13728  metequiv  13998  bj-sseq  14547  bdeq0  14622  bdvsn  14629  bdop  14630  bdeqsuc  14636  bj-om  14692