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

Theorem eloprabga 6402
 Description: The law of concretion for operation class abstraction. Compare elopab 4709. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
Hypothesis
Ref Expression
eloprabga.1
Assertion
Ref Expression
eloprabga
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)   (,,)   (,,)

Proof of Theorem eloprabga
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3040 . 2
2 elex 3040 . 2
3 elex 3040 . 2
4 opex 4664 . . 3
5 simpr 468 . . . . . . . . . 10
65eqeq1d 2473 . . . . . . . . 9
7 eqcom 2478 . . . . . . . . . 10
8 vex 3034 . . . . . . . . . . 11
9 vex 3034 . . . . . . . . . . 11
10 vex 3034 . . . . . . . . . . 11
118, 9, 10otth2 4683 . . . . . . . . . 10
127, 11bitri 257 . . . . . . . . 9
136, 12syl6bb 269 . . . . . . . 8
1413anbi1d 719 . . . . . . 7
15 eloprabga.1 . . . . . . . 8
1615pm5.32i 649 . . . . . . 7
1714, 16syl6bb 269 . . . . . 6
18173exbidv 1779 . . . . 5
19 df-oprab 6312 . . . . . . . . 9
2019eleq2i 2541 . . . . . . . 8
21 abid 2459 . . . . . . . 8
2220, 21bitr2i 258 . . . . . . 7
23 eleq1 2537 . . . . . . 7
2422, 23syl5bb 265 . . . . . 6
2524adantl 473 . . . . 5
26 elisset 3043 . . . . . . . . . 10
27 elisset 3043 . . . . . . . . . 10
28 elisset 3043 . . . . . . . . . 10
2926, 27, 283anim123i 1215 . . . . . . . . 9
30 eeeanv 2094 . . . . . . . . 9
3129, 30sylibr 217 . . . . . . . 8
3231biantrurd 516 . . . . . . 7
33 19.41vvv 1840 . . . . . . 7
3432, 33syl6rbbr 272 . . . . . 6
3534adantr 472 . . . . 5
3618, 25, 353bitr3d 291 . . . 4
3736expcom 442 . . 3
384, 37vtocle 3109 . 2
391, 2, 3, 38syl3an 1334 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904  cab 2457  cvv 3031  cop 3965  coprab 6309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-oprab 6312 This theorem is referenced by:  eloprabg  6403  ovigg  6436  vdwpc  15009  isrgra  25733  isrusgra  25734  elmpps  30283
 Copyright terms: Public domain W3C validator