Metamath Proof Explorer

Theorem ctex

Description: A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016) (Proof shortened by Jim Kingdon, 13-Mar-2023)

Ref Expression
Assertion ctex 
|- ( A ~<_ _om -> A e. _V )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex1i 
 |-  ( A ~<_ _om -> A e. _V )