Description: An identity law for the non-logical predicate, which combines elequ1 and elequ2 . The analogous theorems for class terms are eleq1 , eleq2 , and eleq12 respectively. (Contributed by BJ, 29-Sep-2019)