Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpt3rab1 Structured version   Unicode version

Theorem ovmpt3rab1 6515
 Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
Hypotheses
Ref Expression
ovmpt3rab1.o
ovmpt3rab1.m
ovmpt3rab1.n
ovmpt3rab1.p
ovmpt3rab1.x
ovmpt3rab1.y
Assertion
Ref Expression
ovmpt3rab1
Distinct variable groups:   ,,,   ,,,   ,   ,,   ,,   ,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,)   (,)   ()   ()   (,,,)   (,,)   (,,,)   (,)   (,)

Proof of Theorem ovmpt3rab1
StepHypRef Expression
1 ovmpt3rab1.o . . 3
21a1i 11 . 2
3 ovmpt3rab1.m . . . 4
4 ovmpt3rab1.n . . . . 5
5 ovmpt3rab1.p . . . . 5
64, 5rabeqbidv 3088 . . . 4
73, 6mpteq12dv 4511 . . 3
9 eqidd 2442 . 2
10 elex 3102 . . 3
12 elex 3102 . . 3
14 mptexg 6123 . . 3
16 nfv 1692 . 2
17 nfv 1692 . 2
18 nfcv 2603 . 2
19 nfcv 2603 . 2
20 nfcv 2603 . . 3
21 ovmpt3rab1.x . . . 4
22 nfcv 2603 . . . 4
2321, 22nfrab 3023 . . 3
2420, 23nfmpt 4521 . 2
25 nfcv 2603 . . 3
26 ovmpt3rab1.y . . . 4
27 nfcv 2603 . . . 4
2826, 27nfrab 3023 . . 3
2925, 28nfmpt 4521 . 2
302, 8, 9, 11, 13, 15, 16, 17, 18, 19, 24, 29ovmpt2dxf 6409 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 972   wceq 1381  wnf 1601   wcel 1802  crab 2795  cvv 3093   cmpt 4491  (class class class)co 6277   cmpt2 6279 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pr 4672 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282 This theorem is referenced by:  ovmpt3rabdm  6516  elovmpt3rab1  6517
 Copyright terms: Public domain W3C validator