Metamath Proof Explorer

Theorem ovprc

Description: The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis ovprc1.1 Rel dom F
Assertion ovprc ¬ A V B V A F B =


Step Hyp Ref Expression
1 ovprc1.1 Rel dom F
2 df-ov A F B = F A B
3 df-br A dom F B A B dom F
4 1 brrelex12i A dom F B A V B V
5 3 4 sylbir A B dom F A V B V
6 ndmfv ¬ A B dom F F A B =
7 5 6 nsyl5 ¬ A V B V F A B =
8 2 7 syl5eq ¬ A V B V A F B =