**Description:** Two classes that are related by a binary relation are sets. Inference
form. (Contributed by BJ, 3-Oct-2022)

Ref | Expression | ||
---|---|---|---|

Hypothesis | brrelexi.1 | $${\u22a2}\mathrm{Rel}{R}$$ | |

Assertion | brrelex12i | $${\u22a2}{A}{R}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | brrelexi.1 | $${\u22a2}\mathrm{Rel}{R}$$ | |

2 | brrelex12 | $${\u22a2}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$$ | |

3 | 1 2 | mpan | $${\u22a2}{A}{R}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$$ |