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

Theorem brovmpt2ex 6825
Description: A binary relation of the value of an operation given by the "maps to" notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
Hypothesis
Ref Expression
brovmpt2ex.1
Assertion
Ref Expression
brovmpt2ex
Distinct variable group:   , , ,

Proof of Theorem brovmpt2ex
StepHypRef Expression
1 brovmpt2ex.1 . 2
21relmpt2opab 6739 . . 3
32a1i 11 . 2
41, 3brovex 6824 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1757   cvv 3052   class class class wbr 4374  {copab 4431  Relwrel 4927  (class class class)co 6174  e.cmpt2 6176
This theorem is referenced by:  2mwlk  23546  wlkbprop  23552  trliswlk  23557  pthistrl  23590  spthispth  23591  pthdepisspth  23592  wlkdvspth  23626  crctistrl  23633  cyclispth  23634  cycliscrct  23635  cyclnspth  23636  iseupa  23705  eupatrl  23708  isclwlkg  30542  clwlkiswlk  30544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fv 5508  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-1st 6661  df-2nd 6662
  Copyright terms: Public domain W3C validator