This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A class abstraction based on a class abstraction based on a set is a
set. (Contributed by AV, 16-Jul-2019) (Revised by AV, 26-Mar-2021)
|
|
Ref |
Expression |
|
Hypotheses |
rab2ex.1 |
|- B = { y e. A | ps } |
|
|
rab2ex.2 |
|- A e. _V |
|
Assertion |
rab2ex |
|- { x e. B | ph } e. _V |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rab2ex.1 |
|- B = { y e. A | ps } |
| 2 |
|
rab2ex.2 |
|- A e. _V |
| 3 |
1 2
|
rabex2 |
|- B e. _V |
| 4 |
3
|
rabex |
|- { x e. B | ph } e. _V |