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  3831  unidif  3919  ssunieq  3920  iuneq1  3977  iuneq2  3980  iunxdif2  4013  ssext  4306  pweqb  4308  eqopab2b  4367  pwunim  4374  soeq2  4404  iunpw  4568  ordunisuc2r  4603  tfi  4671  eqrel  4805  eqrelrel  4817  coeq1  4876  coeq2  4877  cnveq  4893  dmeq  4920  relssres  5039  xp11m  5163  xpcanm  5164  xpcan2m  5165  ssrnres  5167  fnres  5436  eqfnfv3  5727  fneqeql2  5737  fconst4m  5852  f1imaeq  5892  eqoprab2b  6053  fo1stresm  6297  fo2ndresm  6298  nnacan  6648  nnmcan  6655  ixpeq2  6849  sbthlemi3  7114  wrdeq  11080  isprm2  12625  lssle0  14321  bastop1  14742  epttop  14749  opnneiid  14823  cnntr  14884  metequiv  15154  bj-sseq  16086  bdeq0  16160  bdvsn  16167  bdop  16168  bdeqsuc  16174  bj-om  16230