Definition df-prrngo

Description: Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	df-prrngo	⊢ PrRing = { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprrng	⊢ PrRing
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		cgi	⊢ GId
4		c1st	⊢ 1st
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( 1st ‘ 𝑟 )
7	6 3	cfv	⊢ ( GId ‘ ( 1st ‘ 𝑟 ) )
8	7	csn	⊢ { ( GId ‘ ( 1st ‘ 𝑟 ) ) }
9		cpridl	⊢ PrIdl
10	5 9	cfv	⊢ ( PrIdl ‘ 𝑟 )
11	8 10	wcel	⊢ { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 )
12	11 1 2	crab	⊢ { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) }
13	0 12	wceq	⊢ PrRing = { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) }