Theorem epelon2

Description: Over the ordinal numbers, one may define the relation A _E B iff A e. B and one finds that, under this ordering, On is a well-ordered class, see epweon . This is a weak form of epelg which only requires that we know B to be a set. (Contributed by RP, 27-Sep-2023)

	Ref	Expression
Assertion	epelon2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		epelg	$$⊢B\in \mathrm{On}\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$
2	1	adantl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\mathrm{E}B\leftrightarrow A\in B\right)$$