Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemg2cN Structured version   Unicode version

Theorem cdlemg2cN 31386
 Description: Any translation belongs to the set of functions constructed for cdleme 31357. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemg2.b
cdlemg2.l
cdlemg2.j
cdlemg2.m
cdlemg2.a
cdlemg2.h
cdlemg2.t
cdlemg2.u
cdlemg2.d
cdlemg2.e
cdlemg2.g
Assertion
Ref Expression
cdlemg2cN
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   (,,,,)   (,)   (,,,,)   (,,,,)

Proof of Theorem cdlemg2cN
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cdlemg2.l . . 3
2 cdlemg2.a . . 3
3 cdlemg2.h . . 3
4 cdlemg2.t . . 3
51, 2, 3, 4cdlemg1cN 31384 . 2
6 cdlemg2.b . . . . 5
7 cdlemg2.j . . . . 5
8 cdlemg2.m . . . . 5
9 cdlemg2.u . . . . 5
10 cdlemg2.d . . . . 5
11 cdlemg2.e . . . . 5
12 cdlemg2.g . . . . 5
13 eqid 2436 . . . . 5
146, 1, 7, 8, 2, 3, 9, 10, 11, 12, 4, 13cdlemg1b2 31368 . . . 4