Theorem eqss 3252

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 2226	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		ssalel 3225	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		ssalel 3225	. . 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 2203   ⊆ wss 3210

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  eqssi  3253  eqssd  3254  sseq1  3260  sseq2  3261  eqimss  3291  ssrabeq  3325  uneqin  3471  ss0b  3547  vss  3555  sssnm  3857  unidif  3945  ssunieq  3946  iuneq1  4003  iuneq2  4006  iunxdif2  4039  ssext  4336  pweqb  4338  eqopab2b  4397  pwunim  4406  soeq2  4436  iunpw  4600  ordunisuc2r  4635  tfi  4703  eqrel  4838  eqrelrel  4850  coeq1  4911  coeq2  4912  cnveq  4928  dmeq  4955  relssres  5075  xp11m  5200  xpcanm  5201  xpcan2m  5202  ssrnres  5204  fnres  5474  eqfnfv3  5776  fneqeql2  5786  fconst4m  5903  f1imaeq  5947  eqoprab2b  6110  fo1stresm  6354  fo2ndresm  6355  nnacan  6744  nnmcan  6751  ixpeq2  6946  sbthlemi3  7228  wrdeq  11242  isprm2  12810  lssle0  14512  bastop1  14940  epttop  14947  opnneiid  15021  cnntr  15082  metequiv  15352  bj-sseq  16556  bdeq0  16629  bdvsn  16636  bdop  16637  bdeqsuc  16643  bj-om  16699