Theorem bnj918

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj918.1	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
Assertion	bnj918	⊢ 𝐺 ∈ V

Proof

Step	Hyp	Ref	Expression
1		bnj918.1	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
2		vex	⊢ 𝑓 ∈ V
3		snex	⊢ { ⟨ 𝑛 , 𝐶 ⟩ } ∈ V
4	2 3	unex	⊢ ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) ∈ V
5	1 4	eqeltri	⊢ 𝐺 ∈ V