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	⊢ ( 𝑍 ∈ GoldbachEven ↔ ( 𝑍 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 = ( 𝑝 + 𝑞 ) ↔ 𝑍 = ( 𝑝 + 𝑞 ) ) )
2	1	3anbi3d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) ) ↔ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) )
3	2	2rexbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) )
4		df-gbe	⊢ GoldbachEven = { 𝑧 ∈ Even ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) ) }
5	3 4	elrab2	⊢ ( 𝑍 ∈ GoldbachEven ↔ ( 𝑍 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) )