Metamath Proof Explorer


Theorem el7g

Description: Members of a set with seven elements. Lemma for usgrexmpl2nb0 etc. (Contributed by AV, 9-Aug-2025)

Ref Expression
Assertion el7g X V X A B C D E F G X = A X = B X = C X = D X = E X = F X = G

Proof

Step Hyp Ref Expression
1 elun X A B C D E F G X A X B C D E F G
2 elsng X V X A X = A
3 elun X B C D E F G X B C D X E F G
4 eltpg X V X B C D X = B X = C X = D
5 eltpg X V X E F G X = E X = F X = G
6 4 5 orbi12d X V X B C D X E F G X = B X = C X = D X = E X = F X = G
7 3 6 bitrid X V X B C D E F G X = B X = C X = D X = E X = F X = G
8 2 7 orbi12d X V X A X B C D E F G X = A X = B X = C X = D X = E X = F X = G
9 1 8 bitrid X V X A B C D E F G X = A X = B X = C X = D X = E X = F X = G