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