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 𝑅 | |
Assertion | brrelex12i | ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | ⊢ Rel 𝑅 | |
2 | brrelex12 | ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) | |
3 | 1 2 | mpan | ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |