Theorem eqss 3243

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2202   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqssi  3244  eqssd  3245  sseq1  3251  sseq2  3252  eqimss  3282  ssrabeq  3316  uneqin  3460  ss0b  3536  vss  3544  sssnm  3842  unidif  3930  ssunieq  3931  iuneq1  3988  iuneq2  3991  iunxdif2  4024  ssext  4319  pweqb  4321  eqopab2b  4380  pwunim  4389  soeq2  4419  iunpw  4583  ordunisuc2r  4618  tfi  4686  eqrel  4821  eqrelrel  4833  coeq1  4893  coeq2  4894  cnveq  4910  dmeq  4937  relssres  5057  xp11m  5182  xpcanm  5183  xpcan2m  5184  ssrnres  5186  fnres  5456  eqfnfv3  5755  fneqeql2  5765  fconst4m  5882  f1imaeq  5926  eqoprab2b  6089  fo1stresm  6333  fo2ndresm  6334  nnacan  6723  nnmcan  6730  ixpeq2  6924  sbthlemi3  7201  wrdeq  11182  isprm2  12750  lssle0  14448  bastop1  14874  epttop  14881  opnneiid  14955  cnntr  15016  metequiv  15286  bj-sseq  16490  bdeq0  16563  bdvsn  16570  bdop  16571  bdeqsuc  16577  bj-om  16633