Theorem onprcALT

Description: Alternate proof of onprc from onprcr . (Contributed by Adrian Ducourtial, 15-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onprcALT	⊢ ¬ On ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-on	⊢ On = { 𝑥 ∣ Ord 𝑥 }
2		rabab	⊢ { 𝑥 ∈ V ∣ Ord 𝑥 } = { 𝑥 ∣ Ord 𝑥 }
3	1 2	eqtr4i	⊢ On = { 𝑥 ∈ V ∣ Ord 𝑥 }
4		tron	⊢ Tr On
5	3 4	onprcr	⊢ ¬ On ∈ V