Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovmpt3rabdm Structured version   Unicode version

Theorem ovmpt3rabdm 30115
 Description: If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019.)
Hypotheses
Ref Expression
ovmpt3rab1.o
ovmpt3rab1.m
ovmpt3rab1.n
Assertion
Ref Expression
ovmpt3rabdm
Distinct variable groups:   ,,,   ,,,   ,   ,,   ,,   ,,   ,,,,   ,,,,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,)   ()   ()   (,,,)   (,,)   (,,,)   ()   ()

Proof of Theorem ovmpt3rabdm
StepHypRef Expression
1 ovmpt3rab1.o . . . . 5
2 ovmpt3rab1.m . . . . 5
3 ovmpt3rab1.n . . . . 5
4 sbceq1a 3192 . . . . . 6
5 sbceq1a 3192 . . . . . 6
64, 5sylan9bbr 700 . . . . 5
7 nfcv 2574 . . . . . 6
87nfsbc1 3200 . . . . 5
9 nfcv 2574 . . . . . 6
10 nfcv 2574 . . . . . . 7
1110nfsbc1 3200 . . . . . 6
129, 11nfsbc 3203 . . . . 5
131, 2, 3, 6, 8, 12ovmpt3rab1 30114 . . . 4