Metamath Proof Explorer

Theorem brrelex12i

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 
|- Rel R
Assertion brrelex12i 
|- ( A R B -> ( A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 brrelexi.1 
 |-  Rel R
2 brrelex12 
 |-  ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
3 1 2 mpan 
 |-  ( A R B -> ( A e. _V /\ B e. _V ) )