Description: The value of a class exists. Inference form of fvex . (Contributed by Glauco Siliprandi, 23-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | fvexi.1 | ⊢ 𝐴 = ( 𝐹 ‘ 𝐵 ) | |
| Assertion | fvexi | ⊢ 𝐴 ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvexi.1 | ⊢ 𝐴 = ( 𝐹 ‘ 𝐵 ) | |
| 2 | fvex | ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V | |
| 3 | 1 2 | eqeltri | ⊢ 𝐴 ∈ V |