Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eloprabga Unicode version

Theorem eloprabga 5866
 Description: The law of concretion for operation class abstraction. Compare elopab 4188. (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 2700 . 2
2 elex 2700 . 2
3 elex 2700 . 2
4 opexg 4158 . . . . 5
5 opexg 4158 . . . . 5
64, 5sylan 281 . . . 4
763impa 1177 . . 3
8 simpr 109 . . . . . . . . . . 11
98eqeq1d 2149 . . . . . . . . . 10
10 eqcom 2142 . . . . . . . . . . 11
11 vex 2692 . . . . . . . . . . . 12
12 vex 2692 . . . . . . . . . . . 12
13 vex 2692 . . . . . . . . . . . 12
1411, 12, 13otth2 4171 . . . . . . . . . . 11
1510, 14bitri 183 . . . . . . . . . 10
169, 15syl6bb 195 . . . . . . . . 9
1716anbi1d 461 . . . . . . . 8
18 eloprabga.1 . . . . . . . . 9
1918pm5.32i 450 . . . . . . . 8
2017, 19syl6bb 195 . . . . . . 7
21203exbidv 1842 . . . . . 6
22 df-oprab 5786 . . . . . . . . . 10
2322eleq2i 2207 . . . . . . . . 9
24 abid 2128 . . . . . . . . 9
2523, 24bitr2i 184 . . . . . . . 8
26 eleq1 2203 . . . . . . . 8
2725, 26syl5bb 191 . . . . . . 7
2827adantl 275 . . . . . 6
29 19.41vvv 1877 . . . . . . . 8
30 elisset 2703 . . . . . . . . . . 11
31 elisset 2703 . . . . . . . . . . 11
32 elisset 2703 . . . . . . . . . . 11
3330, 31, 323anim123i 1167 . . . . . . . . . 10
34 eeeanv 1906 . . . . . . . . . 10
3533, 34sylibr 133 . . . . . . . . 9
3635biantrurd 303 . . . . . . . 8
3729, 36bitr4id 198 . . . . . . 7
3837adantr 274 . . . . . 6
3921, 28, 383bitr3d 217 . . . . 5
4039expcom 115 . . . 4
4140vtocleg 2760 . . 3
427, 41mpcom 36 . 2
431, 2, 3, 42syl3an 1259 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332  wex 1469   wcel 1481  cab 2126  cvv 2689  cop 3535  coprab 5783 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-oprab 5786 This theorem is referenced by:  eloprabg  5867  ovigg  5899
 Copyright terms: Public domain W3C validator