Theorem isgbe

Description: The predicate "is an even Goldbach number". An even Goldbach number is an even integer having a Goldbach partition, i.e. which can be written as a sum of two odd primes. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	isgbe	|- ( Z e. GoldbachEven <-> ( Z e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( z = Z -> ( z = ( p + q ) <-> Z = ( p + q ) ) )
2	1	3anbi3d	|- ( z = Z -> ( ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) <-> ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )
3	2	2rexbidv	|- ( z = Z -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) <-> E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )
4		df-gbe	|- GoldbachEven = { z e. Even | E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) }
5	3 4	elrab2	|- ( Z e. GoldbachEven <-> ( Z e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )