Theorem elirrvALT

Description: Alternate proof of elirrv , shorter but using more axioms. (Contributed by BTernaryTau, 28-Dec-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elirrvALT	$$⊢\neg x\in x$$

Proof

Step	Hyp	Ref	Expression
1		zfregfr	$$⊢\mathrm{E}\mathrm{Fr}x$$
2		efrirr	$$⊢\mathrm{E}\mathrm{Fr}x\to \neg x\in x$$
3	1 2	ax-mp	$$⊢\neg x\in x$$