Metamath Proof Explorer

Theorem bj-brrelex12ALT

Description: Two classes related by a binary relation are both sets. Alternate proof of brrelex12 . (Contributed by BJ, 14-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-brrelex12ALT ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 0nelrel0 ⊢ Rel ⁡ R → ¬ ∅ ∈ R
2 jcn ⊢ A R B → ¬ ∅ ∈ R → ¬ A R B → ∅ ∈ R
3 2 impcom ⊢ ¬ ∅ ∈ R ∧ A R B → ¬ A R B → ∅ ∈ R
4 opprc ⊢ ¬ A ∈ V ∧ B ∈ V → A B = ∅
5 df-br ⊢ A R B ↔ A B ∈ R
6 5 biimpi ⊢ A R B → A B ∈ R
7 eleq1 ⊢ A B = ∅ → A B ∈ R ↔ ∅ ∈ R
8 6 7 imbitrid ⊢ A B = ∅ → A R B → ∅ ∈ R
9 4 8 syl ⊢ ¬ A ∈ V ∧ B ∈ V → A R B → ∅ ∈ R
10 3 9 nsyl2 ⊢ ¬ ∅ ∈ R ∧ A R B → A ∈ V ∧ B ∈ V
11 1 10 sylan ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V