Metamath Proof Explorer


Theorem atsseq

Description: Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atsseq A HAtoms B HAtoms A B A = B

Proof

Step Hyp Ref Expression
1 atne0 A HAtoms A 0
2 1 ad2antrr A HAtoms B HAtoms A B A 0
3 atelch A HAtoms A C
4 atss A C B HAtoms A B A = B A = 0
5 3 4 sylan A HAtoms B HAtoms A B A = B A = 0
6 5 imp A HAtoms B HAtoms A B A = B A = 0
7 6 ord A HAtoms B HAtoms A B ¬ A = B A = 0
8 7 necon1ad A HAtoms B HAtoms A B A 0 A = B
9 2 8 mpd A HAtoms B HAtoms A B A = B
10 9 ex A HAtoms B HAtoms A B A = B
11 eqimss A = B A B
12 10 11 impbid1 A HAtoms B HAtoms A B A = B