This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nprrel

Description: No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005)

Ref Expression
Hypotheses nprrel12.1 ⊢ Rel ⁡ R
nprrel.2 ⊢ ¬ A ∈ V
Assertion nprrel ⊢ ¬ A R B

Proof

Step Hyp Ref Expression
1 nprrel12.1 ⊢ Rel ⁡ R
2 nprrel.2 ⊢ ¬ A ∈ V
3 1 brrelex1i ⊢ A R B → A ∈ V
4 2 3 mto ⊢ ¬ A R B