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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elequ12 | |- ( ( x = y /\ z = t ) -> ( x e. z <-> y e. t ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elequ1 | |- ( x = y -> ( x e. z <-> y e. z ) ) |
|
| 2 | elequ2 | |- ( z = t -> ( y e. z <-> y e. t ) ) |
|
| 3 | 1 2 | sylan9bb | |- ( ( x = y /\ z = t ) -> ( x e. z <-> y e. t ) ) |