Theorem eqss 3239

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 3212	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		ssalel 3212	. . 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 3197

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 3203  df-ss 3210

This theorem is referenced by:  eqssi  3240  eqssd  3241  sseq1  3247  sseq2  3248  eqimss  3278  ssrabeq  3311  uneqin  3455  ss0b  3531  vss  3539  sssnm  3832  unidif  3920  ssunieq  3921  iuneq1  3978  iuneq2  3981  iunxdif2  4014  ssext  4308  pweqb  4310  eqopab2b  4369  pwunim  4378  soeq2  4408  iunpw  4572  ordunisuc2r  4607  tfi  4675  eqrel  4810  eqrelrel  4822  coeq1  4882  coeq2  4883  cnveq  4899  dmeq  4926  relssres  5046  xp11m  5170  xpcanm  5171  xpcan2m  5172  ssrnres  5174  fnres  5443  eqfnfv3  5739  fneqeql2  5749  fconst4m  5866  f1imaeq  5908  eqoprab2b  6071  fo1stresm  6316  fo2ndresm  6317  nnacan  6671  nnmcan  6678  ixpeq2  6872  sbthlemi3  7142  wrdeq  11111  isprm2  12660  lssle0  14357  bastop1  14778  epttop  14785  opnneiid  14859  cnntr  14920  metequiv  15190  bj-sseq  16265  bdeq0  16339  bdvsn  16346  bdop  16347  bdeqsuc  16353  bj-om  16409