Description: A variant of relopabiv (which could be proved from it, similarly to relxp from xpss ). (Contributed by BJ, 28-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-opabssvv | |- { <. x , y >. | ph } C_ ( _V X. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | vex | |- y e. _V |
|
| 3 | 1 2 | pm3.2i | |- ( x e. _V /\ y e. _V ) |
| 4 | 3 | a1i | |- ( ph -> ( x e. _V /\ y e. _V ) ) |
| 5 | 4 | ssopab2i | |- { <. x , y >. | ph } C_ { <. x , y >. | ( x e. _V /\ y e. _V ) } |
| 6 | df-xp | |- ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) } |
|
| 7 | 5 6 | sseqtrri | |- { <. x , y >. | ph } C_ ( _V X. _V ) |