Description: Lemma for elisset and isset . (Contributed by NM, 26-May-1993) Extract from the proof of isset . (Revised by WL, 2-Feb-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | issetlem.1 | ||
Assertion | issetlem |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issetlem.1 | ||
2 | dfclel | ||
3 | 1 | biantru | |
4 | 3 | exbii | |
5 | 2 4 | bitr4i |