Theorem predasetex

Description: The predecessor class exists when A does. (Contributed by Scott Fenton, 8-Feb-2011)

	Ref	Expression
Hypothesis	predasetex.1	⊢ 𝐴 ∈ V
Assertion	predasetex	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		predasetex.1	⊢ 𝐴 ∈ V
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3	1	inex1	⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∈ V
4	2 3	eqeltri	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V